src/HOL/Library/Continuity.thy
changeset 46508 ec9630fe9ca7
parent 44928 7ef6505bde7f
child 54257 5c7a3b6b05a9
--- a/src/HOL/Library/Continuity.thy	Thu Feb 16 22:53:24 2012 +0100
+++ b/src/HOL/Library/Continuity.thy	Thu Feb 16 22:53:56 2012 +0100
@@ -5,7 +5,7 @@
 header {* Continuity and iterations (of set transformers) *}
 
 theory Continuity
-imports Transitive_Closure Main
+imports Main
 begin
 
 subsection {* Continuity for complete lattices *}