src/ZF/IsaMakefile
changeset 6053 8a1059aa01f0
parent 5561 426c1e330903
child 6065 3b4a29166f26
     1.1 --- a/src/ZF/IsaMakefile	Mon Dec 28 16:58:11 1998 +0100
     1.2 +++ b/src/ZF/IsaMakefile	Mon Dec 28 16:59:28 1998 +0100
     1.3 @@ -38,12 +38,12 @@
     1.4    Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \
     1.5    Rel.thy Sum.ML Sum.thy Trancl.ML Trancl.thy \
     1.6    Update.ML Update.thy Univ.ML Univ.thy WF.ML WF.thy \
     1.7 -  ZF.ML ZF.thy Zorn.ML Zorn.thy add_ind_def.ML add_ind_def.thy \
     1.8 -  cartprod.ML cartprod.thy constructor.ML constructor.thy domrange.ML \
     1.9 +  ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML \
    1.10    domrange.thy equalities.ML equalities.thy func.ML func.thy \
    1.11 -  ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \
    1.12 -  intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
    1.13 -  subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy \
    1.14 +  ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
    1.15 +  subset.thy thy_syntax.ML upair.ML upair.thy \
    1.16 +  Tools/cartprod.ML Tools/datatype_package.ML Tools/inductive_package.ML \
    1.17 +  Tools/primrec_package.ML Tools/typechk.ML \
    1.18    Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \
    1.19    Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy 
    1.20  	@$(ISATOOL) usedir -b $(OUT)/FOL ZF
    1.21 @@ -96,7 +96,7 @@
    1.22    Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \
    1.23    Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \
    1.24    Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \
    1.25 -  Resid/SubUnion.ML Resid/SubUnion.thy Resid/Substitution.ML \
    1.26 +  Resid/Substitution.ML \
    1.27    Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy
    1.28  	@$(ISATOOL) usedir $(OUT)/ZF Resid
    1.29  
    1.30 @@ -111,6 +111,7 @@
    1.31    ex/Enum.thy ex/LList.ML ex/LList.thy \
    1.32    ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \
    1.33    ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
    1.34 +  ex/Primrec_defs.ML ex/Primrec_defs.thy \
    1.35    ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \
    1.36    ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \
    1.37    ex/Term.ML ex/Term.thy ex/misc.ML