src/ZF/IsaMakefile
changeset 5539 25e743eef48a
parent 5464 47d0d906b39a
child 5561 426c1e330903
     1.1 --- a/src/ZF/IsaMakefile	Wed Sep 23 10:15:09 1998 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Wed Sep 23 10:17:11 1998 +0200
     1.3 @@ -29,8 +29,8 @@
     1.4  $(OUT)/ZF: $(OUT)/FOL $(SRC)/Pure/section_utils.ML AC.ML AC.thy \
     1.5    Arith.ML Arith.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \
     1.6    CardinalArith.ML CardinalArith.thy Cardinal_AC.ML Cardinal_AC.thy \
     1.7 -  Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy EquivClass.ML \
     1.8 -  EquivClass.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy \
     1.9 +  Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy \
    1.10 +  Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy \
    1.11    Inductive.ML Inductive.thy InfDatatype.ML InfDatatype.thy \
    1.12    Let.ML Let.thy List.ML List.thy Main.thy Nat.ML Nat.thy \
    1.13    Order.ML Order.thy OrderArith.ML \
    1.14 @@ -43,7 +43,9 @@
    1.15    domrange.thy equalities.ML equalities.thy func.ML func.thy \
    1.16    ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \
    1.17    intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
    1.18 -  subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy
    1.19 +  subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy \
    1.20 +  Integ/EquivClass.ML Integ/EquivClass.thy Integ/Integ.ML Integ/Integ.thy \
    1.21 +  Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy 
    1.22  	@$(ISATOOL) usedir -b $(OUT)/FOL ZF
    1.23  
    1.24  
    1.25 @@ -104,14 +106,14 @@
    1.26  ZF-ex: ZF $(LOG)/ZF-ex.gz
    1.27  
    1.28  $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \
    1.29 -  ex/Bin.ML ex/Bin.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
    1.30 +  ex/BinEx.ML ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
    1.31    ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Data.ML ex/Data.thy ex/Enum.ML \
    1.32 -  ex/Enum.thy ex/Integ.ML ex/Integ.thy ex/LList.ML ex/LList.thy \
    1.33 +  ex/Enum.thy ex/LList.ML ex/LList.thy \
    1.34    ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \
    1.35    ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
    1.36    ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \
    1.37    ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \
    1.38 -  ex/Term.ML ex/Term.thy ex/misc.ML ex/twos_compl.ML ex/twos_compl.thy
    1.39 +  ex/Term.ML ex/Term.thy ex/misc.ML
    1.40  	@$(ISATOOL) usedir $(OUT)/ZF ex
    1.41  
    1.42