| #
97b2ecf5 |
|
08-Nov-2018 |
haftmann <none@none> |
removed relics of ASCII syntax for indexed big operators
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
53d65c13 |
|
08-Aug-2016 |
hoelzl <none@none> |
rename HOL-Multivariate_Analysis to HOL-Analysis.
--HG--
rename : src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy => src/HOL/Analysis/Analysis.thy
rename : src/HOL/Multivariate_Analysis/Binary_Product_Measure.thy => src/HOL/Analysis/Binary_Product_Measure.thy
rename : src/HOL/Multivariate_Analysis/Bochner_Integration.thy => src/HOL/Analysis/Bochner_Integration.thy
rename : src/HOL/Multivariate_Analysis/Borel_Space.thy => src/HOL/Analysis/Borel_Space.thy
rename : src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy => src/HOL/Analysis/Bounded_Continuous_Function.thy
rename : src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy => src/HOL/Analysis/Bounded_Linear_Function.thy
rename : src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy => src/HOL/Analysis/Brouwer_Fixpoint.thy
rename : src/HOL/Multivariate_Analysis/Caratheodory.thy => src/HOL/Analysis/Caratheodory.thy
rename : src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy => src/HOL/Analysis/Cartesian_Euclidean_Space.thy
rename : src/HOL/Multivariate_Analysis/Cauchy_Integral_Theorem.thy => src/HOL/Analysis/Cauchy_Integral_Theorem.thy
rename : src/HOL/Multivariate_Analysis/Complete_Measure.thy => src/HOL/Analysis/Complete_Measure.thy
rename : src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy => src/HOL/Analysis/Complex_Analysis_Basics.thy
rename : src/HOL/Multivariate_Analysis/Complex_Transcendental.thy => src/HOL/Analysis/Complex_Transcendental.thy
rename : src/HOL/Multivariate_Analysis/Conformal_Mappings.thy => src/HOL/Analysis/Conformal_Mappings.thy
rename : src/HOL/Multivariate_Analysis/Continuous_Extension.thy => src/HOL/Analysis/Continuous_Extension.thy
rename : src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy => src/HOL/Analysis/Convex_Euclidean_Space.thy
rename : src/HOL/Multivariate_Analysis/Derivative.thy => src/HOL/Analysis/Derivative.thy
rename : src/HOL/Multivariate_Analysis/Determinants.thy => src/HOL/Analysis/Determinants.thy
rename : src/HOL/Multivariate_Analysis/Embed_Measure.thy => src/HOL/Analysis/Embed_Measure.thy
rename : src/HOL/Multivariate_Analysis/Euclidean_Space.thy => src/HOL/Analysis/Euclidean_Space.thy
rename : src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy => src/HOL/Analysis/Extended_Real_Limits.thy
rename : src/HOL/Multivariate_Analysis/Fashoda_Theorem.thy => src/HOL/Analysis/Fashoda_Theorem.thy
rename : src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy => src/HOL/Analysis/Finite_Cartesian_Product.thy
rename : src/HOL/Multivariate_Analysis/Finite_Product_Measure.thy => src/HOL/Analysis/Finite_Product_Measure.thy
rename : src/HOL/Multivariate_Analysis/Gamma_Function.thy => src/HOL/Analysis/Gamma_Function.thy
rename : src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy => src/HOL/Analysis/Generalised_Binomial_Theorem.thy
rename : src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy => src/HOL/Analysis/Harmonic_Numbers.thy
rename : src/HOL/Multivariate_Analysis/Henstock_Kurzweil_Integration.thy => src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
rename : src/HOL/Multivariate_Analysis/Homeomorphism.thy => src/HOL/Analysis/Homeomorphism.thy
rename : src/HOL/Multivariate_Analysis/Integral_Test.thy => src/HOL/Analysis/Integral_Test.thy
rename : src/HOL/Multivariate_Analysis/Interval_Integral.thy => src/HOL/Analysis/Interval_Integral.thy
rename : src/HOL/Multivariate_Analysis/L2_Norm.thy => src/HOL/Analysis/L2_Norm.thy
rename : src/HOL/Multivariate_Analysis/Lebesgue_Integral_Substitution.thy => src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
rename : src/HOL/Multivariate_Analysis/Lebesgue_Measure.thy => src/HOL/Analysis/Lebesgue_Measure.thy
rename : src/HOL/Multivariate_Analysis/Linear_Algebra.thy => src/HOL/Analysis/Linear_Algebra.thy
rename : src/HOL/Multivariate_Analysis/Measurable.thy => src/HOL/Analysis/Measurable.thy
rename : src/HOL/Multivariate_Analysis/Measure_Space.thy => src/HOL/Analysis/Measure_Space.thy
rename : src/HOL/Multivariate_Analysis/Nonnegative_Lebesgue_Integration.thy => src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
rename : src/HOL/Multivariate_Analysis/Norm_Arith.thy => src/HOL/Analysis/Norm_Arith.thy
rename : src/HOL/Multivariate_Analysis/Operator_Norm.thy => src/HOL/Analysis/Operator_Norm.thy
rename : src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy => src/HOL/Analysis/Ordered_Euclidean_Space.thy
rename : src/HOL/Multivariate_Analysis/Path_Connected.thy => src/HOL/Analysis/Path_Connected.thy
rename : src/HOL/Multivariate_Analysis/Poly_Roots.thy => src/HOL/Analysis/Poly_Roots.thy
rename : src/HOL/Multivariate_Analysis/Polytope.thy => src/HOL/Analysis/Polytope.thy
rename : src/HOL/Multivariate_Analysis/Radon_Nikodym.thy => src/HOL/Analysis/Radon_Nikodym.thy
rename : src/HOL/Multivariate_Analysis/Regularity.thy => src/HOL/Analysis/Regularity.thy
rename : src/HOL/Multivariate_Analysis/Set_Integral.thy => src/HOL/Analysis/Set_Integral.thy
rename : src/HOL/Multivariate_Analysis/Sigma_Algebra.thy => src/HOL/Analysis/Sigma_Algebra.thy
rename : src/HOL/Multivariate_Analysis/Summation_Tests.thy => src/HOL/Analysis/Summation_Tests.thy
rename : src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy => src/HOL/Analysis/Topology_Euclidean_Space.thy
rename : src/HOL/Multivariate_Analysis/Uniform_Limit.thy => src/HOL/Analysis/Uniform_Limit.thy
rename : src/HOL/Multivariate_Analysis/Weierstrass_Theorems.thy => src/HOL/Analysis/Weierstrass_Theorems.thy
rename : src/HOL/Multivariate_Analysis/document/root.tex => src/HOL/Analysis/document/root.tex
rename : src/HOL/Multivariate_Analysis/ex/Approximations.thy => src/HOL/Analysis/ex/Approximations.thy
rename : src/HOL/Multivariate_Analysis/measurable.ML => src/HOL/Analysis/measurable.ML
rename : src/HOL/Multivariate_Analysis/normarith.ML => src/HOL/Analysis/normarith.ML
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
da01cc11 |
|
08-Jan-2016 |
hoelzl <none@none> |
add uniform spaces
|
| #
8e83c9d2 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
c1893073 |
|
05-Mar-2013 |
hoelzl <none@none> |
use generate_topology for second countable topologies, does not require intersection stable basis
|
| #
2732ee62 |
|
31-Jan-2013 |
hoelzl <none@none> |
use order topology for extended reals
|
| #
23578d8d |
|
14-Jan-2013 |
hoelzl <none@none> |
renamed countable_basis_space to second_countable_topology
--HG--
extra : rebase_source : 1287b8162fd3311e5100ce1912cb58896edfb3a5
|
| #
21822db4 |
|
27-Nov-2012 |
immler <none@none> |
based countable topological basis on Countable_Set
--HG--
extra : rebase_source : 326111b06e0d89bbbef5c168b8314ab6023d8fb2
|
| #
7b05f4cc |
|
15-Nov-2012 |
immler <none@none> |
generalized to copy of countable types instead of instantiation of nat for discrete topology
|