# HG changeset patch
# User wenzelm
# Date 924266974 -7200
# Node ID 7c59a55bae941fafd85249da4403a59e22e43bb7
# Parent  7eea9f25dc49e01c9a242d1c905cf8a67b28fd0a
added Tools/induct_method.ML;

diff -r 7eea9f25dc49 -r 7c59a55bae94 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 16 14:49:09 1999 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 16 14:49:34 1999 +0200
@@ -52,7 +52,7 @@
   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/induct_method.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 \
diff -r 7eea9f25dc49 -r 7c59a55bae94 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Fri Apr 16 14:49:09 1999 +0200
+++ b/src/HOL/ROOT.ML	Fri Apr 16 14:49:34 1999 +0200
@@ -56,12 +56,14 @@
 use "Tools/record_package.ML";
 use_thy "Record";
 
+(*TFL: recursive function definitions*)
+use_thy "WF_Rel";
+cd "../TFL";
+use "sys.sml";
+cd "../HOL";
+use "Tools/recdef_package.ML";
+use "Tools/induct_method.ML";
 use_thy "Recdef";
-(*TFL: recursive function definitions*)
-cd "~~/src/TFL";
-use "sys.sml";
-cd "~~/src/HOL";
-use "Tools/recdef_package.ML";
 
 cd "Integ";
 use_thy "IntDef";