src/ZF/IsaMakefile
changeset 22814 4cd25f1706bb
parent 17935 c6f1442ce949
child 23146 0bc590051d95
     1.1 --- a/src/ZF/IsaMakefile	Thu Apr 26 15:41:49 2007 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Thu Apr 26 15:42:04 2007 +0200
     1.3 @@ -28,24 +28,18 @@
     1.4  FOL:
     1.5  	@cd $(SRC)/FOL; $(ISATOOL) make FOL
     1.6  
     1.7 -$(OUT)/ZF$(ML_SUFFIX): $(OUT)/FOL$(ML_SUFFIX) AC.thy Arith.thy \
     1.8 -  ArithSimp.thy Bool.thy Cardinal.thy		\
     1.9 -  CardinalArith.thy Cardinal_AC.thy \
    1.10 -  Datatype.ML Datatype.thy Epsilon.thy Finite.thy	\
    1.11 -  Fixedpt.thy Inductive.ML Inductive.thy 	\
    1.12 -  InfDatatype.thy Integ/Bin.thy \
    1.13 -  Integ/EquivClass.thy Integ/Int.thy Integ/IntArith.thy	\
    1.14 -  Integ/IntDiv.thy Integ/int_arith.ML			\
    1.15 -  List.thy Main.ML Main.thy	\
    1.16 -  Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy	\
    1.17 -  OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy	\
    1.18 -  QPair.thy QUniv.thy ROOT.ML	\
    1.19 -  Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
    1.20 -  Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
    1.21 -  Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
    1.22 -  Trancl.thy Univ.thy \
    1.23 -  WF.thy ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy	\
    1.24 -  ind_syntax.ML pair.thy simpdata.ML upair.thy
    1.25 +$(OUT)/ZF$(ML_SUFFIX): $(OUT)/FOL$(ML_SUFFIX) AC.thy Arith.thy			\
    1.26 +  ArithSimp.thy Bool.thy Cardinal.thy CardinalArith.thy Cardinal_AC.thy		\
    1.27 +  Datatype.thy Epsilon.thy Finite.thy Fixedpt.thy Inductive.thy			\
    1.28 +  InfDatatype.thy Integ/Bin.thy Integ/EquivClass.thy Integ/Int.thy		\
    1.29 +  Integ/IntArith.thy Integ/IntDiv.thy Integ/int_arith.ML List.thy		\
    1.30 +  Main.thy Main_ZFC.thy Nat.thy OrdQuant.thy Order.thy OrderArith.thy		\
    1.31 +  OrderType.thy Ordinal.thy Perm.thy QPair.thy QUniv.thy ROOT.ML Sum.thy	\
    1.32 +  Tools/cartprod.ML Tools/datatype_package.ML Tools/ind_cases.ML		\
    1.33 +  Tools/induct_tacs.ML Tools/inductive_package.ML				\
    1.34 +  Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML		\
    1.35 +  Trancl.thy Univ.thy WF.thy ZF.thy Zorn.thy arith_data.ML			\
    1.36 +  equalities.thy func.thy ind_syntax.ML pair.thy simpdata.ML upair.thy
    1.37  	@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
    1.38  
    1.39