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