load / setup datatype package;

--- 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