| Sun, 13 Apr 2025 23:00:55 +0100 |
paulson |
Tidied some proofs
|
file |
diff |
annotate
|
| Tue, 16 Jan 2024 13:40:09 +0000 |
paulson |
A few new results (mostly brought in from other developments)
|
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, 10 Jul 2023 12:48:26 +0100 |
paulson |
A bit of prerelease tidying
|
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, 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
|
| Sat, 06 May 2023 12:42:10 +0100 |
paulson |
fixes esp to theory presentation
|
file |
diff |
annotate
|
| Sat, 06 May 2023 11:10:23 +0100 |
paulson |
new material ported from HOL Light's metric.ml
|
file |
diff |
annotate
|