| Wed, 28 May 2025 17:49:22 +0200 |
haftmann |
more modern qualification of auxiliary operations
|
file |
diff |
annotate
|
| Sun, 23 Mar 2025 19:26:23 +0000 |
paulson |
Function space instead of image closure
|
file |
diff |
annotate
|
| Wed, 11 Oct 2023 17:02:33 +0100 |
paulson |
atin now an abbreviation for atin_within, which has been moved to Abstract_Limits
|
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 18:30:54 +0100 |
paulson |
more small simplifications
|
file |
diff |
annotate
|
| Sun, 09 Jul 2023 11:38:25 +0100 |
paulson |
Last of the HOL Light metric space imports, and some supporting lemmas
|
file |
diff |
annotate
|
| Wed, 05 Jul 2023 16:50:07 +0100 |
paulson |
A couple of new lemmas involving cardinality
|
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
|
| Tue, 27 Jun 2023 11:56:31 +0100 |
paulson |
More metric space material
|
file |
diff |
annotate
|
| Mon, 26 Jun 2023 14:38:19 +0100 |
paulson |
New and generalised analysis lemmas
|
file |
diff |
annotate
|
| Tue, 30 May 2023 14:24:09 +0100 |
paulson |
Hiding the constructor names, particularly to avoid conflicts involving "ext"
|
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
|