src/HOL/Library/Continuity.thy
changeset 30663 0b6aff7451b2
parent 27487 c8a6ce181805
child 30950 1435a8f01a41
--- a/src/HOL/Library/Continuity.thy	Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Continuity.thy	Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Continuity.thy
-    ID:         $Id$
     Author:     David von Oheimb, TU Muenchen
 *)
 
 header {* Continuity and iterations (of set transformers) *}
 
 theory Continuity
-imports Plain "~~/src/HOL/Relation_Power"
+imports Relation_Power Main
 begin
 
 subsection {* Continuity for complete lattices *}