author  paulson 
Fri, 11 Aug 2000 13:27:17 +0200  
changeset 9578  ab26d6c8ebfe 
parent 9570  e16e168984e1 
child 9647  e9623f47275b 
permissions  rwrr 
2500  1 
# 
2 
# $Id$ 

3 
# 

4 
# IsaMakefile for ZF 

5 
# 

6 

4518  7 
## targets 
2500  8 

4518  9 
default: ZF 
10 
images: ZF 

11 
test: ZFIMP ZFCoind ZFAC ZFResid ZFex 

12 
all: images test 

13 

14 

15 
## global settings 

16 

17 
SRC = $(ISABELLE_HOME)/src 

3118  18 
OUT = $(ISABELLE_OUTPUT) 
4447  19 
LOG = $(OUT)/log 
2500  20 

4518  21 

22 
## ZF 

23 

24 
ZF: FOL $(OUT)/ZF 

25 

26 
FOL: 

27 
@cd $(SRC)/FOL; $(ISATOOL) make FOL 

2500  28 

9548  29 
$(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy Bool.ML \ 
30 
arith_data.ML ArithSimp.thy ArithSimp.ML Bool.thy \ 

8812  31 
Cardinal.ML Cardinal.thy CardinalArith.ML CardinalArith.thy \ 
32 
Cardinal_AC.ML Cardinal_AC.thy Datatype.ML Datatype.thy Epsilon.ML \ 

33 
Epsilon.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy Inductive.ML \ 

9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
9570
diff
changeset

34 
Inductive.thy InfDatatype.ML InfDatatype.thy \ 
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
9570
diff
changeset

35 
Integ/Bin.ML Integ/Bin.thy \ 
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
9570
diff
changeset

36 
Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \ 
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
9570
diff
changeset

37 
Integ/IntDiv.ML Integ/IntDiv.thy \ 
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
9570
diff
changeset

38 
Integ/twos_compl.ML Integ/int_arith.ML Integ/IntArith.thy \ 
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

39 
Let.ML Let.thy List.ML List.thy \ 
8812  40 
Main.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML \ 
41 
OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \ 

42 
Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML \ 

9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

43 
Rel.ML Rel.thy Sum.ML Sum.thy \ 
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

44 
Tools/numeral_syntax.ML Tools/cartprod.ML \ 
8812  45 
Tools/datatype_package.ML Tools/induct_tacs.ML \ 
46 
Tools/inductive_package.ML Tools/primrec_package.ML Tools/typechk.ML \ 

47 
Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML \ 

48 
WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML domrange.thy \ 

49 
equalities.ML equalities.thy func.ML func.thy ind_syntax.ML mono.ML \ 

50 
mono.thy pair.ML pair.thy simpdata.ML subset.ML subset.thy \ 

51 
thy_syntax.ML upair.ML upair.thy 

6213  52 
@$(ISATOOL) usedir b r $(OUT)/FOL ZF 
2500  53 

54 

4518  55 
## ZFIMP 
2500  56 

4518  57 
ZFIMP: ZF $(LOG)/ZFIMP.gz 
2500  58 

4518  59 
$(LOG)/ZFIMP.gz: $(OUT)/ZF IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \ 
60 
IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/ROOT.ML 

2828  61 
@$(ISATOOL) usedir $(OUT)/ZF IMP 
2500  62 

63 

4518  64 
## ZFCoind 
2500  65 

4518  66 
ZFCoind: ZF $(LOG)/ZFCoind.gz 
2500  67 

4518  68 
$(LOG)/ZFCoind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \ 
69 
Coind/ECR.ML Coind/ECR.thy Coind/Language.thy Coind/MT.ML Coind/MT.thy \ 

70 
Coind/Map.ML Coind/Map.thy Coind/ROOT.ML Coind/Static.ML \ 

71 
Coind/Static.thy Coind/Types.ML Coind/Types.thy Coind/Values.ML \ 

72 
Coind/Values.thy 

2828  73 
@$(ISATOOL) usedir $(OUT)/ZF Coind 
2500  74 

75 

4518  76 
## ZFAC 
2500  77 

4518  78 
ZFAC: ZF $(LOG)/ZFAC.gz 
2500  79 

4518  80 
$(LOG)/ZFAC.gz: $(OUT)/ZF AC/AC0_AC1.ML AC/AC10_AC15.ML \ 
81 
AC/AC15_WO6.ML AC/AC15_WO6.thy AC/AC16_WO4.ML AC/AC16_WO4.thy \ 

82 
AC/AC16_lemmas.ML AC/AC16_lemmas.thy AC/AC17_AC1.ML AC/AC17_AC1.thy \ 

83 
AC/AC18_AC19.ML AC/AC18_AC19.thy AC/AC1_AC17.ML AC/AC1_WO2.ML \ 

84 
AC/AC1_WO2.thy AC/AC2_AC6.ML AC/AC7_AC9.ML AC/AC_Equiv.ML \ 

85 
AC/AC_Equiv.thy AC/Cardinal_aux.ML AC/Cardinal_aux.thy AC/DC.ML \ 

86 
AC/DC.thy AC/DC_lemmas.ML AC/DC_lemmas.thy AC/HH.ML AC/HH.thy \ 

87 
AC/Hartog.ML AC/Hartog.thy AC/ROOT.ML AC/WO1_AC.ML AC/WO1_AC.thy \ 

5464  88 
AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO7.thy AC/WO1_WO8.ML AC/WO2_AC16.ML \ 
4518  89 
AC/WO2_AC16.thy AC/WO6_WO1.ML AC/WO6_WO1.thy AC/WO_AC.ML AC/WO_AC.thy \ 
90 
AC/recfunAC16.ML AC/recfunAC16.thy AC/rel_is_fun.ML AC/rel_is_fun.thy 

2828  91 
@$(ISATOOL) usedir $(OUT)/ZF AC 
2500  92 

93 

4518  94 
## ZFResid 
95 

96 
ZFResid: ZF $(LOG)/ZFResid.gz 

2500  97 

4518  98 
$(LOG)/ZFResid.gz: $(OUT)/ZF Resid/Confluence.ML Resid/Confluence.thy \ 
99 
Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \ 

100 
Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \ 

101 
Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \ 

6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
5561
diff
changeset

102 
Resid/Substitution.ML \ 
4518  103 
Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy 
2828  104 
@$(ISATOOL) usedir $(OUT)/ZF Resid 
2500  105 

106 

4518  107 
## ZFex 
108 

109 
ZFex: ZF $(LOG)/ZFex.gz 

2500  110 

4518  111 
$(LOG)/ZFex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \ 
5539  112 
ex/BinEx.ML ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ 
4518  113 
ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Data.ML ex/Data.thy ex/Enum.ML \ 
5539  114 
ex/Enum.thy ex/LList.ML ex/LList.thy \ 
4518  115 
ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \ 
116 
ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \ 

6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
5561
diff
changeset

117 
ex/Primrec_defs.ML ex/Primrec_defs.thy \ 
4518  118 
ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \ 
119 
ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \ 

5539  120 
ex/Term.ML ex/Term.thy ex/misc.ML 
2828  121 
@$(ISATOOL) usedir $(OUT)/ZF ex 
2500  122 

123 

4518  124 
## clean 
4447  125 

126 
clean: 

4518  127 
@rm f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZFIMP.gz \ 
128 
$(LOG)/ZFCoind.gz $(LOG)/ZFAC.gz $(LOG)/ZFResid.gz \ 

129 
$(LOG)/ZFex.gz 