src/HOL/Topological_Spaces.thy
changeset 51773 9328c6681f3c
parent 51641 cd05e9fcc63d
child 51774 916271d52466
--- a/src/HOL/Topological_Spaces.thy	Thu Apr 25 10:31:10 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed Apr 24 13:28:30 2013 +0200
@@ -6,7 +6,7 @@
 header {* Topological Spaces *}
 
 theory Topological_Spaces
-imports Main Conditional_Complete_Lattices
+imports Main Conditionally_Complete_Lattices
 begin
 
 subsection {* Topological space *}
@@ -2079,7 +2079,7 @@
 
 section {* Connectedness *}
 
-class linear_continuum_topology = linorder_topology + conditional_complete_linorder + inner_dense_linorder
+class linear_continuum_topology = linorder_topology + conditionally_complete_linorder + inner_dense_linorder
 begin
 
 lemma Inf_notin_open: