src/HOL/Topological_Spaces.thy
changeset 51773 9328c6681f3c
parent 51641 cd05e9fcc63d
child 51774 916271d52466
     1.1 --- a/src/HOL/Topological_Spaces.thy	Thu Apr 25 10:31:10 2013 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Apr 24 13:28:30 2013 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Topological Spaces *}
     1.5  
     1.6  theory Topological_Spaces
     1.7 -imports Main Conditional_Complete_Lattices
     1.8 +imports Main Conditionally_Complete_Lattices
     1.9  begin
    1.10  
    1.11  subsection {* Topological space *}
    1.12 @@ -2079,7 +2079,7 @@
    1.13  
    1.14  section {* Connectedness *}
    1.15  
    1.16 -class linear_continuum_topology = linorder_topology + conditional_complete_linorder + inner_dense_linorder
    1.17 +class linear_continuum_topology = linorder_topology + conditionally_complete_linorder + inner_dense_linorder
    1.18  begin
    1.19  
    1.20  lemma Inf_notin_open: