| Tue, 15 Apr 2025 17:38:20 +0200 |
Manuel Eberl |
lots of lemmas for HOL, HOL-{Complex_}Analysis, HOL-Number_Theory
|
file |
diff |
annotate
|
| Fri, 04 Apr 2025 16:37:58 +0100 |
paulson |
Inserted more of Manuel Eberl's material
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Thu, 28 Mar 2024 13:32:57 +0000 |
paulson |
An assortment of new material, mostly due to Manuel
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 17:06:05 +0100 |
paulson |
A few new theorems
|
file |
diff |
annotate
|
| Mon, 21 Aug 2023 18:38:25 +0100 |
paulson |
Numerous minor tweaks and simplifications
|
file |
diff |
annotate
|
| Sat, 15 Jul 2023 23:34:42 +0100 |
paulson |
trivial_topology
|
file |
diff |
annotate
|
| Tue, 11 Jul 2023 20:21:58 +0100 |
paulson |
cosmetic improvements, new lemmas, especially more uses of function space
|
file |
diff |
annotate
|
| Mon, 03 Jul 2023 11:45:59 +0100 |
paulson |
EXPERIMENTAL replacement of f ` A <= B by f : A -> B in Analysis
|
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
|
| Mon, 02 Jan 2023 20:46:24 +0000 |
paulson |
Tidying up of paths, introducing "loop_free" as a separate predicate in the definition of "simple_path"
|
file |
diff |
annotate
|
| Sun, 01 Jan 2023 01:43:02 +0000 |
paulson |
A couple of patches
|
file |
diff |
annotate
|
| Sun, 01 Jan 2023 00:45:55 +0000 |
paulson |
Big simplifications of old proofs
|
file |
diff |
annotate
|
| Thu, 05 Aug 2021 07:12:49 +0000 |
haftmann |
clarified abstract and concrete boolean algebras
|
file |
diff |
annotate
|
| Fri, 16 Jul 2021 14:43:25 +0100 |
paulson |
A few new lemmas and simplifications
|
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
|
| Thu, 03 Jun 2021 10:47:20 +0100 |
paulson |
new lemmas mostly about paths
|
file |
diff |
annotate
|
| Fri, 11 Sep 2020 14:14:58 +0100 |
paulson |
cleaned up some messy proofs
|
file |
diff |
annotate
|
| Sun, 30 Aug 2020 19:45:46 +0100 |
paulson |
minor tidying, also s->S and t->T
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 17:03:58 +0100 |
nipkow |
cleaning
|
file |
diff |
annotate
|
| Thu, 05 Dec 2019 11:21:17 +0100 |
nipkow |
made Starlike independent of Abstract_Limits
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 22:40:16 -0500 |
immler |
split off metric spaces part of Function_Topology: subsequent theories Product_Topology, T1_Spaces, Lindelof_Spaces are purely topological
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 10:31:51 +0100 |
Manuel Eberl |
Merged
|
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
|
| Sun, 01 Dec 2019 19:10:57 +0000 |
Wenda Li |
renamed Analysis/Winding_Numbers to Winding_Numbers_2; reorganised Analysis/Cauchy_Integral_Theorem by splitting it into Contour_Integration, Winding_Numbers,Cauchy_Integral_Theorem and Cauchy_Integral_Formula.
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Mon, 04 Nov 2019 17:18:25 -0500 |
immler |
reduce dependencies of Ordered_Euclidean_Space; move more general material from Cartesian_Euclidean_Space
|
file |
diff |
annotate
|
| Wed, 30 Oct 2019 15:26:10 -0400 |
immler |
linear is not needed
|
file |
diff |
annotate
|