# HG changeset patch
# User wenzelm
# Date 939066225 -7200
# Node ID 38b6d264363071967272ea93ff49858f4ea89e1b
# Parent  09d8fd81cc1f5b76e14b6a9ea8267840d4226d11
load / setup datatype package;

diff -r 09d8fd81cc1f -r 38b6d2643630 src/HOL/Inductive.thy
--- 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