src/HOL/Analysis/Analysis.thy
2 months ago paulson 2019-03-22 New abstract topological material
3 months ago paulson 2019-03-19 new material about topology, etc.; also fixes for yesterday's
3 months ago paulson 2019-03-07 new material for Analysis
5 months ago immler 2019-01-16 chapters for analysis manual
8 months ago paulson 2018-10-17 new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
11 months ago Manuel Eberl 2018-07-13 HOL-Analysis: Volume of a simplex, Heron's theorem
12 months ago paulson 2018-06-18 New material in support of quaternions
14 months ago paulson 2018-04-18 Oops! Change_Of_Vars was not being imported to Analysis!
14 months ago paulson 2018-04-17 Vitali covering theorem
15 months ago immler 2018-02-26 moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
18 months ago eberlm 2017-12-24 Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
20 months ago paulson 2017-10-10 Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.
22 months ago Manuel Eberl 2017-08-21 HOL-Analysis: Convergent FPS and infinite sums
23 months ago paulson 2017-07-26 New theory of Equiintegrability / Continuity of the indefinite integral / improper integration
23 months ago eberlm 2017-07-15 HOL-Analysis: Infinite products
2017-02-22 paulson 2017-02-22 The Great Picard Theorem
2017-02-22 paulson 2017-02-22 New theory about Winding Numbers
2017-01-09 paulson 2017-01-09 Jordan Curve Theorem
2017-01-05 paulson 2017-01-05 New theory of arcwise connected sets and other new material
2016-10-18 hoelzl 2016-10-18 HOL-Analysis: move Function Topology from AFP/Ergodict_Theory; HOL-Probability: move Essential Supremum from AFP/Lp
2016-10-03 paulson 2016-10-03 new theorems including the theory FurtherTopology
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
2016-08-08 hoelzl 2016-08-08 rename HOL-Multivariate_Analysis to HOL-Analysis.