| changeset 77939 | 98879407d33c |
| parent 77935 | 7f240b0dabd9 |
| child 77943 | ffdad62bc235 |
--- a/src/HOL/Analysis/Abstract_Topology.thy Wed May 03 10:35:20 2023 +0100 +++ b/src/HOL/Analysis/Abstract_Topology.thy Wed May 03 11:20:03 2023 +0100 @@ -1,5 +1,4 @@ -(* Author: L C Paulson, University of Cambridge [ported from HOL Light] -*) +(* Author: L C Paulson, University of Cambridge [ported from HOL Light] *) section \<open>Operators involving abstract topology\<close>