src/ZF/Datatype.thy

--- a/src/ZF/Datatype.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Datatype.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -7,9 +7,9 @@
 
 header{*Datatype and CoDatatype Definitions*}
 
-theory Datatype = Inductive + Univ + QUniv
-  files
+theory Datatype imports Inductive Univ QUniv
+  uses
     "Tools/datatype_package.ML"
-    "Tools/numeral_syntax.ML":  (*belongs to theory Bin*)
+    "Tools/numeral_syntax.ML" begin  (*belongs to theory Bin*)
 
 end