Wed, 16 Jan 2019 19:34:48 -0500 |
immler |
chapters for analysis manual
|
file |
diff |
annotate
|
Wed, 17 Oct 2018 14:19:07 +0100 |
paulson |
new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
|
file |
diff |
annotate
|
Fri, 13 Jul 2018 18:27:18 +0100 |
Manuel Eberl |
HOL-Analysis: Volume of a simplex, Heron's theorem
|
file |
diff |
annotate
|
Mon, 18 Jun 2018 14:22:26 +0100 |
paulson |
New material in support of quaternions
|
file |
diff |
annotate
|
Wed, 18 Apr 2018 18:46:51 +0100 |
paulson |
Oops! Change_Of_Vars was not being imported to Analysis!
|
file |
diff |
annotate
|
Tue, 17 Apr 2018 12:09:23 +0100 |
paulson |
Vitali covering theorem
|
file |
diff |
annotate
|
Mon, 26 Feb 2018 07:34:05 +0100 |
immler |
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
|
file |
diff |
annotate
|
Sun, 24 Dec 2017 14:28:10 +0100 |
eberlm |
Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
|
file |
diff |
annotate
|
Tue, 10 Oct 2017 14:03:51 +0100 |
paulson |
Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.
|
file |
diff |
annotate
|
Mon, 21 Aug 2017 20:49:15 +0200 |
Manuel Eberl |
HOL-Analysis: Convergent FPS and infinite sums
|
file |
diff |
annotate
|
Wed, 26 Jul 2017 16:07:45 +0100 |
paulson |
New theory of Equiintegrability / Continuity of the indefinite integral / improper integration
|
file |
diff |
annotate
|
Sat, 15 Jul 2017 14:33:56 +0100 |
eberlm |
HOL-Analysis: Infinite products
|
file |
diff |
annotate
|
Wed, 22 Feb 2017 16:21:26 +0000 |
paulson |
The Great Picard Theorem
|
file |
diff |
annotate
|
Wed, 22 Feb 2017 15:04:59 +0000 |
paulson |
New theory about Winding Numbers
|
file |
diff |
annotate
|
Mon, 09 Jan 2017 14:40:31 +0000 |
paulson |
Jordan Curve Theorem
|
file |
diff |
annotate
|
Thu, 05 Jan 2017 16:03:23 +0000 |
paulson |
New theory of arcwise connected sets and other new material
|
file |
diff |
annotate
|
Tue, 18 Oct 2016 17:29:28 +0200 |
hoelzl |
HOL-Analysis: move Function Topology from AFP/Ergodict_Theory; HOL-Probability: move Essential Supremum from AFP/Lp
|
file |
diff |
annotate
|
Mon, 03 Oct 2016 13:01:01 +0100 |
paulson |
new theorems including the theory FurtherTopology
|
file |
diff |
annotate
|
Fri, 30 Sep 2016 11:35:39 +0200 |
hoelzl |
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)
|
file |
diff |
annotate
|
Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
| base
|