| 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
|
| Tue, 04 Jul 2023 12:53:01 +0100 |
paulson |
Another tranche of HOL Light material on metric and topological spaces
|
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
|
| Mon, 26 Jun 2023 14:38:19 +0100 |
paulson |
New and generalised analysis lemmas
|
file |
diff |
annotate
|
| Tue, 30 May 2023 12:33:06 +0100 |
paulson |
New HOL Light material on metric spaces and topological spaces
|
file |
diff |
annotate
|
| Tue, 23 May 2023 12:31:23 +0100 |
paulson |
Finally, the abstract metric space development
|
file |
diff |
annotate
|
| Thu, 18 May 2023 11:44:42 +0100 |
paulson |
New material from the HOL Light metric space library, mostly about quasi components
|
file |
diff |
annotate
|
| Mon, 15 May 2023 17:12:18 +0100 |
paulson |
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
|
| Wed, 03 May 2023 11:20:03 +0100 |
paulson |
Two new theories containing material ported from HOL Light about abstract topology
|
file |
diff |
annotate
|
| Tue, 02 May 2023 15:17:39 +0100 |
paulson |
More new theorems, and a necessary correction
|
file |
diff |
annotate
|
| Tue, 02 May 2023 12:51:05 +0100 |
paulson |
A few new theorems
|
file |
diff |
annotate
|
| Sun, 12 Feb 2023 20:49:31 +0000 |
paulson |
Simplification of proofs
|
file |
diff |
annotate
|
| Tue, 17 May 2022 14:10:14 +0100 |
paulson |
tidied auto / simp with null arguments
|
file |
diff |
annotate
|
| Thu, 05 May 2022 16:39:48 +0100 |
paulson |
Added a couple of obvious simprules
|
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, 15 Nov 2020 13:06:24 +0000 |
paulson |
more de-applying
|
file |
diff |
annotate
|
| Sat, 23 May 2020 21:24:33 +0100 |
paulson |
a few new lemmas about functions
|
file |
diff |
annotate
|
| Thu, 14 May 2020 13:44:44 +0200 |
Manuel Eberl |
Tuned some proofs in HOL-Analysis
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:11:56 +0100 |
paulson |
new material; rotated premises of Lim_transform_eventually
|
file |
diff |
annotate
|
| Fri, 03 May 2019 15:43:02 +0100 |
paulson |
tweaked a definition
|
file |
diff |
annotate
|
| Wed, 17 Apr 2019 17:48:28 +0100 |
paulson |
Lindelöf spaces and supporting material
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Mon, 08 Apr 2019 15:26:54 +0100 |
paulson |
First tranche of the Homology development: Simplices
|
file |
diff |
annotate
|
| Fri, 05 Apr 2019 15:02:46 +0100 |
paulson |
Free_Abelian_Groups finally working; fixed some duplicates; cleaned up some proofs
|
file |
diff |
annotate
|
| Thu, 04 Apr 2019 14:19:33 +0100 |
paulson |
More group theory. Sum and product indexed by the non-neutral part of a set
|
file |
diff |
annotate
|
| Wed, 27 Mar 2019 14:08:26 +0000 |
paulson |
more stuff from HOL Light: Euclidean spaces and n-spheres, Hausdorff spaces, etc.
|
file |
diff |
annotate
|
| Tue, 26 Mar 2019 17:01:36 +0000 |
paulson |
generalised homotopic_with to topologies; homotopic_with_canon is the old version
|
file |
diff |
annotate
|
| Fri, 22 Mar 2019 12:34:49 +0000 |
paulson |
New abstract topological material
|
file |
diff |
annotate
|
| Thu, 21 Mar 2019 14:18:22 +0000 |
paulson |
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
|
file |
diff |
annotate
|
| Tue, 19 Mar 2019 16:14:51 +0000 |
paulson |
new material about topology, etc.; also fixes for yesterday's
|
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
|
| Thu, 07 Mar 2019 14:08:05 +0000 |
paulson |
new material for Analysis
|
file |
diff |
annotate
|
| Mon, 28 Jan 2019 10:27:47 +0100 |
nipkow |
more canonical and less specialized syntax
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 10:50:35 +0000 |
paulson |
some renamings and a bit of new material
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 18:50:41 +0100 |
immler |
moved generalized lemmas
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 12:32:01 +0100 |
nipkow |
typed definitions
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 20:32:09 +0100 |
immler |
split off theorems involving classes below metric_space and real_normed_vector
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 15:43:53 +0100 |
nipkow |
capitalize proper names in lemma names
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 19:48:28 +0100 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
| Thu, 22 Nov 2018 10:06:31 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Sun, 11 Nov 2018 16:08:59 +0100 |
nipkow |
tuned
|
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
|