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