| Tue, 03 Oct 2023 15:01:54 +0100 |
paulson |
New proofs also some slightly faster existing proofs
|
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
|
| Thu, 06 Jul 2023 16:59:12 +0100 |
paulson |
The sym_diff operator (symmetric difference)
|
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
|
| Thu, 01 Jun 2023 12:08:33 +0100 |
paulson |
Even more material from the HOL Light metric space library
|
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
|