| Thu, 01 Jun 2023 12:08:33 +0100 |
paulson |
Even more material from the HOL Light metric space library
|
file |
diff |
annotate
|
| Sun, 07 May 2023 14:52:53 +0100 |
paulson |
Importation of additional lemmas from metric.ml
|
file |
diff |
annotate
|
| Tue, 07 Feb 2023 14:10:08 +0000 |
paulson |
More new theorems from the number theory development
|
file |
diff |
annotate
|
| Thu, 26 Jan 2023 13:59:51 +0000 |
paulson |
Moved in some material from the AFP entry Winding_number_eval
|
file |
diff |
annotate
|
| Wed, 21 Dec 2022 12:30:48 +0000 |
paulson |
Additional new material about infinite products, etc.
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 12:42:51 +0100 |
paulson |
A few new lemmas plus some refinements
|
file |
diff |
annotate
|
| Wed, 06 Oct 2021 14:19:46 +0200 |
eberlm |
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
|
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
|
| Tue, 08 Sep 2020 15:30:15 +0100 |
paulson |
tidying and de-applying
|
file |
diff |
annotate
|
| Thu, 27 Aug 2020 15:23:48 +0100 |
paulson |
but not the [cong] rule
|
file |
diff |
annotate
|
| Thu, 27 Aug 2020 12:14:46 +0100 |
paulson |
tidying up some theorem statements
|
file |
diff |
annotate
|
| Wed, 13 May 2020 12:55:33 +0200 |
Manuel Eberl |
new constant power_int in HOL
|
file |
diff |
annotate
|
| Mon, 11 May 2020 11:15:41 +0100 |
paulson |
the Uniq quantifier
|
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
|
| 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
|
| Wed, 09 Oct 2019 15:32:41 +0100 |
paulson |
More theorems about limits, including cancellation simprules
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:39:10 +0100 |
paulson |
Generalised two results concerning limits from the real numbers to type classes
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 14:41:37 +0100 |
paulson |
imported new material mostly due to Sébastien Gouëzel
|
file |
diff |
annotate
|
| Fri, 13 Sep 2019 12:46:36 +0100 |
paulson |
New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours
|
file |
diff |
annotate
|
| Thu, 12 Sep 2019 14:51:45 +0100 |
paulson |
new material on Analysis, plus some rearrangements
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:11:56 +0100 |
paulson |
new material; rotated premises of Lim_transform_eventually
|
file |
diff |
annotate
|
| Wed, 17 Jul 2019 14:02:42 +0100 |
paulson |
a few new lemmas and a bit of tidying
|
file |
diff |
annotate
|
| Mon, 18 Mar 2019 15:35:34 +0000 |
paulson |
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 22:29:09 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Thu, 30 Aug 2018 17:20:54 +0200 |
Manuel Eberl |
Some basic materials on filters and topology
|
file |
diff |
annotate
|
| Sat, 04 Aug 2018 01:03:39 +0200 |
eberlm |
Small lemmas about analysis
|
file |
diff |
annotate
|