--- 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 \
--- 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";