--- a/src/HOL/Inductive.thy Mon Oct 04 21:43:05 1999 +0200
+++ b/src/HOL/Inductive.thy Mon Oct 04 21:43:45 1999 +0200
@@ -1,7 +1,19 @@
+(* Title: HOL/Inductive.thy
+ ID: $Id$
+*)
theory Inductive = Gfp + Prod + Sum
-files "Tools/inductive_package.ML":
+files
+ "Tools/inductive_package.ML"
+ "Tools/datatype_aux.ML"
+ "Tools/datatype_prop.ML"
+ "Tools/datatype_rep_proofs.ML"
+ "Tools/datatype_abs_proofs.ML"
+ "Tools/datatype_package.ML"
+ "Tools/primrec_package.ML":
setup InductivePackage.setup
+setup DatatypePackage.setup
+
end