| Thu, 03 Aug 2023 19:10:36 +0200 |
paulson |
More cosmetic changes
|
file |
diff |
annotate
|
| Wed, 01 Feb 2023 12:43:33 +0000 |
paulson |
More new material thanks to Manuel
|
file |
diff |
annotate
|
| Tue, 31 Jan 2023 14:05:16 +0000 |
paulson |
Lots more new material thanks to Manuel Eberl
|
file |
diff |
annotate
|
| Fri, 30 Dec 2022 17:48:41 +0000 |
paulson |
A further round of proof consolidation
|
file |
diff |
annotate
|
| Tue, 15 Feb 2022 13:00:05 +0000 |
paulson |
an assortment of new or stronger lemmas
|
file |
diff |
annotate
|
| Wed, 05 Jan 2022 15:35:23 +0000 |
paulson |
New and simplified theorems
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:44:18 +0200 |
desharna |
merged
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Sun, 04 Jul 2021 18:35:57 +0100 |
paulson |
Imported lots of material from Stirling_Formula/Gamma_Asymptotics
|
file |
diff |
annotate
|
| Mon, 28 Jun 2021 15:05:46 +0100 |
paulson |
A few useful lemmas about derivatives, colinearity and other topics
|
file |
diff |
annotate
|
| Thu, 03 Jun 2021 10:47:20 +0100 |
paulson |
new lemmas mostly about paths
|
file |
diff |
annotate
|
| Wed, 11 Nov 2020 14:27:17 +0000 |
paulson |
mult_le_cancel_iff1, mult_le_cancel_iff2, mult_less_iff1 generalised from the real_ versions
|
file |
diff |
annotate
|
| Sun, 11 Oct 2020 14:56:03 +0100 |
paulson |
tidying and removal of legacy name
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Sat, 30 Nov 2019 13:47:33 +0100 |
Manuel Eberl |
Split off new HOL-Complex_Analysis session from HOL-Analysis
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 15:06:04 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 18:40:39 +0100 |
nipkow |
reduced imports
|
file |
diff |
annotate
|
| Tue, 26 Nov 2019 14:32:08 +0000 |
paulson |
Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.
|
file |
diff |
annotate
|
| Mon, 04 Nov 2019 19:53:43 -0500 |
immler |
Line_Segment is independent of Convex_Euclidean_Space
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 21:42:45 +0000 |
paulson |
moved line segments to Convex_Euclidean_Space
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 14:31:34 +0000 |
paulson |
Inverse function theorem + lemmas
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Tue, 08 Oct 2019 10:26:40 +0000 |
haftmann |
formally augmented corresponding rules for field_simps
|
file |
diff |
annotate
|
| Thu, 19 Sep 2019 17:24:08 +0100 |
paulson |
Tidying and one more theorem
|
file |
diff |
annotate
|
| Thu, 19 Sep 2019 13:59:29 +0100 |
paulson |
Four new results from Smooth_Manifolds/Analysis_More
|
file |
diff |
annotate
|
| Wed, 04 Sep 2019 14:16:27 +0100 |
paulson |
Theory Derivative no longer depends on Path_Connected
|
file |
diff |
annotate
|
| Wed, 28 Aug 2019 00:08:14 +0200 |
immler |
removed Brouwer_Fixpoint from imports of Derivative
|
file |
diff |
annotate
|
| Tue, 27 Aug 2019 17:08:51 +0200 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:11:56 +0100 |
paulson |
new material; rotated premises of Lim_transform_eventually
|
file |
diff |
annotate
|
| Fri, 19 Jul 2019 12:57:14 +0100 |
paulson |
More results about measure and integration theory
|
file |
diff |
annotate
|