| #
a4784f6f |
|
09-Oct-2019 |
haftmann <none@none> |
dedicated fact collections for algebraic simplification rules potentially splitting goals
--HG--
extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6
|
| #
f504d7e3 |
|
10-Apr-2019 |
paulson <lp15@cam.ac.uk> |
prod/sum fixes
|
| #
35216754 |
|
10-Apr-2019 |
paulson <lp15@cam.ac.uk> |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
| #
48a391b7 |
|
10-Apr-2019 |
paulson <lp15@cam.ac.uk> |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
593ff4b4 |
|
17-Oct-2016 |
nipkow <none@none> |
setprod -> prod
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
9a8c3fb3 |
|
19-Sep-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
| #
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
|