--- 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: