src/ZF/IsaMakefile
changeset 8812 7239b21e2068
parent 6213 f5bdd6497e08
child 9548 15bee2731e43
     1.1 --- a/src/ZF/IsaMakefile	Fri May 05 22:24:47 2000 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Fri May 05 22:25:17 2000 +0200
     1.3 @@ -26,26 +26,24 @@
     1.4  FOL:
     1.5  	@cd $(SRC)/FOL; $(ISATOOL) make FOL
     1.6  
     1.7 -$(OUT)/ZF: $(OUT)/FOL $(SRC)/Pure/section_utils.ML AC.ML AC.thy \
     1.8 -  Arith.ML Arith.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \
     1.9 -  CardinalArith.ML CardinalArith.thy Cardinal_AC.ML Cardinal_AC.thy \
    1.10 -  Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy \
    1.11 -  Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy \
    1.12 -  Inductive.ML Inductive.thy InfDatatype.ML InfDatatype.thy \
    1.13 -  Let.ML Let.thy List.ML List.thy Main.thy Nat.ML Nat.thy \
    1.14 -  Order.ML Order.thy OrderArith.ML \
    1.15 -  OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \
    1.16 -  Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \
    1.17 -  Rel.thy Sum.ML Sum.thy Trancl.ML Trancl.thy \
    1.18 -  Update.ML Update.thy Univ.ML Univ.thy WF.ML WF.thy \
    1.19 -  ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML \
    1.20 -  domrange.thy equalities.ML equalities.thy func.ML func.thy \
    1.21 -  ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
    1.22 -  subset.thy thy_syntax.ML upair.ML upair.thy \
    1.23 -  Tools/cartprod.ML Tools/datatype_package.ML Tools/inductive_package.ML \
    1.24 -  Tools/primrec_package.ML Tools/induct_tacs.ML Tools/typechk.ML \
    1.25 -  Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \
    1.26 -  Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy 
    1.27 +$(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy Bool.ML Bool.thy	\
    1.28 +  Cardinal.ML Cardinal.thy CardinalArith.ML CardinalArith.thy		\
    1.29 +  Cardinal_AC.ML Cardinal_AC.thy Datatype.ML Datatype.thy Epsilon.ML	\
    1.30 +  Epsilon.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy Inductive.ML	\
    1.31 +  Inductive.thy InfDatatype.ML InfDatatype.thy Integ/Bin.ML		\
    1.32 +  Integ/Bin.thy Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML	\
    1.33 +  Integ/Int.thy Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy	\
    1.34 +  Main.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML		\
    1.35 +  OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy	\
    1.36 +  Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML	\
    1.37 +  Rel.ML Rel.thy Sum.ML Sum.thy Tools/cartprod.ML			\
    1.38 +  Tools/datatype_package.ML Tools/induct_tacs.ML			\
    1.39 +  Tools/inductive_package.ML Tools/primrec_package.ML Tools/typechk.ML	\
    1.40 +  Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML	\
    1.41 +  WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML domrange.thy		\
    1.42 +  equalities.ML equalities.thy func.ML func.thy ind_syntax.ML mono.ML	\
    1.43 +  mono.thy pair.ML pair.thy simpdata.ML subset.ML subset.thy		\
    1.44 +  thy_syntax.ML upair.ML upair.thy
    1.45  	@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
    1.46  
    1.47