src/HOL/Library/Accessible_Part.thy

--- a/src/HOL/Library/Accessible_Part.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Accessible_Part.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,8 +6,9 @@
 
 header {* The accessible part of a relation *}
 
-theory Accessible_Part = Main:
-
+theory Accessible_Part
+import Main
+begin
 
 subsection {* Inductive definition *}