| Thu, 01 Jun 2023 12:08:33 +0100 | paulson | Even more material from the HOL Light metric space library | file | diff | annotate |
| Thu, 08 Jul 2021 08:42:36 +0200 | desharna | added opaque_combs and renamed hide_lams to opaque_lifting | file | diff | annotate |
| Tue, 31 Mar 2020 15:51:15 +0200 | nipkow | cleaned proofs | file | diff | annotate |
| Mon, 02 Dec 2019 22:40:16 -0500 | immler | split off metric spaces part of Function_Topology: subsequent theories Product_Topology, T1_Spaces, Lindelof_Spaces are purely topological | file | diff | annotate |