| 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 |