#
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
|