src/HOL/Topological_Spaces.thy
changeset 52265 bb907eba5902
parent 51775 408d937c9486
child 52729 412c9e0381a1
equal deleted inserted replaced
52264:cdba0c3cb4c2 52265:bb907eba5902
     1 (*  Title:      HOL/Basic_Topology.thy
     1 (*  Title:      HOL/Topological_Spaces.thy
     2     Author:     Brian Huffman
     2     Author:     Brian Huffman
     3     Author:     Johannes Hölzl
     3     Author:     Johannes Hölzl
     4 *)
     4 *)
     5 
     5 
     6 header {* Topological Spaces *}
     6 header {* Topological Spaces *}