# HG changeset patch
# User wenzelm
# Date 924109624 -7200
# Node ID a42bdc45130daf3e931948ce5dfd95077eb0b291
# Parent  69400c97d3bf627aaf367692ab061beaea0d271b
Tools/inductive_package.ML;

diff -r 69400c97d3bf -r a42bdc45130d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Apr 14 19:05:28 1999 +0200
+++ b/src/HOL/IsaMakefile	Wed Apr 14 19:07:04 1999 +0200
@@ -52,12 +52,13 @@
   String.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
   Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
   Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
-  Tools/inductive_package.ML Tools/primrec_package.ML \
+  Tools/inductive_package.ML \
+  Tools/primrec_package.ML Tools/recdef_package.ML \
   Tools/record_package.ML Tools/typedef_package.ML Trancl.ML \
   Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
-  WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML \
-  equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
-  subset.thy thy_syntax.ML
+  WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML equalities.thy \
+  hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \
+  thy_syntax.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
 
 
diff -r 69400c97d3bf -r a42bdc45130d src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Apr 14 19:05:28 1999 +0200
+++ b/src/HOL/ROOT.ML	Wed Apr 14 19:07:04 1999 +0200
@@ -61,6 +61,7 @@
 cd "~~/src/TFL";
 use "sys.sml";
 cd "~~/src/HOL";
+use "Tools/recdef_package.ML";
 
 cd "Integ";
 use_thy "IntDef";