Tools/inductive_package.ML;
authorwenzelm
Wed Apr 14 19:07:04 1999 +0200 (1999-04-14)
changeset 6431a42bdc45130d
parent 6430 69400c97d3bf
child 6432 cdde45202c5c
Tools/inductive_package.ML;
src/HOL/IsaMakefile
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Apr 14 19:05:28 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Apr 14 19:07:04 1999 +0200
     1.3 @@ -52,12 +52,13 @@
     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 Tools/primrec_package.ML \
     1.8 +  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 \
    1.12 -  WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML \
    1.13 -  equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
    1.14 -  subset.thy thy_syntax.ML
    1.15 +  WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML equalities.thy \
    1.16 +  hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \
    1.17 +  thy_syntax.ML
    1.18  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    1.19  
    1.20  
     2.1 --- a/src/HOL/ROOT.ML	Wed Apr 14 19:05:28 1999 +0200
     2.2 +++ b/src/HOL/ROOT.ML	Wed Apr 14 19:07:04 1999 +0200
     2.3 @@ -61,6 +61,7 @@
     2.4  cd "~~/src/TFL";
     2.5  use "sys.sml";
     2.6  cd "~~/src/HOL";
     2.7 +use "Tools/recdef_package.ML";
     2.8  
     2.9  cd "Integ";
    2.10  use_thy "IntDef";