src/ZF/Inductive.thy

--- a/src/ZF/Inductive.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Inductive.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -7,14 +7,14 @@
 
 header{*Inductive and Coinductive Definitions*}
 
-theory Inductive = Fixedpt + QPair
-  files
+theory Inductive imports Fixedpt QPair
+  uses
     "ind_syntax.ML"
     "Tools/cartprod.ML"
     "Tools/ind_cases.ML"
     "Tools/inductive_package.ML"
     "Tools/induct_tacs.ML"
-    "Tools/primrec_package.ML":
+    "Tools/primrec_package.ML" begin
 
 setup IndCases.setup
 setup DatatypeTactics.setup