src/ZF/Makefile
changeset 342 82104a03565a
parent 339 7e67ca1618b7
child 363 1180a3c5479e
equal deleted inserted replaced
341:257fcb40bacc 342:82104a03565a
    18 
    18 
    19 BIN = $(ISABELLEBIN)
    19 BIN = $(ISABELLEBIN)
    20 COMP = $(ISABELLECOMP)
    20 COMP = $(ISABELLECOMP)
    21 FILES = ROOT.ML ZF.thy ZF.ML upair.ML subset.ML pair.ML domrange.ML \
    21 FILES = ROOT.ML ZF.thy ZF.ML upair.ML subset.ML pair.ML domrange.ML \
    22 	func.ML simpdata.ML Bool.thy Bool.ML \
    22 	func.ML simpdata.ML Bool.thy Bool.ML \
    23 	Sum.thy Sum.ML Qpair.thy Qpair.ML mono.ML Fixedpt.thy Fixedpt.ML \
    23 	Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \
    24 	ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \
    24 	ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \
    25 	equalities.ML Perm.thy Perm.ML Trancl.thy Trancl.ML \
    25 	equalities.ML Perm.thy Perm.ML Trancl.thy Trancl.ML \
    26 	WF.thy WF.ML Ord.thy Ord.ML Nat.thy Nat.ML \
    26 	WF.thy WF.ML Ord.thy Ord.ML Nat.thy Nat.ML \
    27 	Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
    27 	Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
    28 	Quniv.thy Quniv.ML constructor.ML datatype.ML  \
    28 	QUniv.thy QUniv.ML constructor.ML Datatype.ML  \
    29 	fin.ML list.ML ListFn.thy ListFn.ML
    29 	fin.ML List.ML ListFn.thy ListFn.ML
    30 
    30 
    31 EX_FILES = ex/ROOT.ML ex/acc.ML ex/bin.ML ex/BinFn.ML ex/BinFn.thy\
    31 EX_FILES = ex/ROOT.ML ex/Acc.ML ex/Bin.ML ex/BinFn.ML ex/BinFn.thy\
    32 	   ex/BT.ML ex/BT_Fn.ML ex/BT_Fn.thy ex/comb.ML\
    32 	   ex/BT.ML ex/BT_Fn.ML ex/BT_Fn.thy ex/Comb.ML\
    33 	   ex/Contract0.ML ex/Contract0.thy ex/counit.ML ex/data.ML\
    33 	   ex/Contract0.ML ex/Contract0.thy ex/counit.ML ex/Data.ML\
    34 	   ex/enum.ML ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\
    34 	   ex/Enum.ML ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\
    35 	   ex/listn.ML ex/llist.ML ex/llist_eq.ML ex/LListFn.ML ex/LListFn.thy\
    35 	   ex/ListN.ML ex/llist.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\
    36 	   ex/misc.ML ex/parcontract.ML ex/Primrec0.ML ex/Primrec0.thy\
    36 	   ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\
    37 	   ex/prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\
    37 	   ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\
    38 	   ex/rmap.ML ex/term.ML ex/TermFn.ML ex/TermFn.thy ex/tf.ML\
    38 	   ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy ex/TF.ML\
    39 	   ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML
    39 	   ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML
    40 
    40 
    41 #Uses cp rather than make_database because Poly/ML allows only 3 levels
    41 #Uses cp rather than make_database because Poly/ML allows only 3 levels
    42 $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
    42 $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
    43 	case "$(COMP)" in \
    43 	case "$(COMP)" in \