added Tools/induct_method.ML;
authorwenzelm
Fri Apr 16 14:49:34 1999 +0200 (1999-04-16)
changeset 64407c59a55bae94
parent 6439 7eea9f25dc49
child 6441 268aa3c4a059
added Tools/induct_method.ML;
src/HOL/IsaMakefile
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Apr 16 14:49:09 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 16 14:49:34 1999 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4    String.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
     1.5    Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
     1.6    Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
     1.7 -  Tools/inductive_package.ML \
     1.8 +  Tools/induct_method.ML Tools/inductive_package.ML \
     1.9    Tools/primrec_package.ML Tools/recdef_package.ML \
    1.10    Tools/record_package.ML Tools/typedef_package.ML Trancl.ML \
    1.11    Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
     2.1 --- a/src/HOL/ROOT.ML	Fri Apr 16 14:49:09 1999 +0200
     2.2 +++ b/src/HOL/ROOT.ML	Fri Apr 16 14:49:34 1999 +0200
     2.3 @@ -56,12 +56,14 @@
     2.4  use "Tools/record_package.ML";
     2.5  use_thy "Record";
     2.6  
     2.7 +(*TFL: recursive function definitions*)
     2.8 +use_thy "WF_Rel";
     2.9 +cd "../TFL";
    2.10 +use "sys.sml";
    2.11 +cd "../HOL";
    2.12 +use "Tools/recdef_package.ML";
    2.13 +use "Tools/induct_method.ML";
    2.14  use_thy "Recdef";
    2.15 -(*TFL: recursive function definitions*)
    2.16 -cd "~~/src/TFL";
    2.17 -use "sys.sml";
    2.18 -cd "~~/src/HOL";
    2.19 -use "Tools/recdef_package.ML";
    2.20  
    2.21  cd "Integ";
    2.22  use_thy "IntDef";