# HG changeset patch
# User wenzelm
# Date 1329429236 -3600
# Node ID ec9630fe9ca77a30aa069fe939d9029a4245107f
# Parent  1b24c24017dd9c9ea64e97f881048c98b4a7e3da
tuned imports;

diff -r 1b24c24017dd -r ec9630fe9ca7 src/HOL/Library/Continuity.thy
--- 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 *}