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