author  wenzelm 
Fri, 05 May 2000 22:25:17 +0200  
changeset 8812  7239b21e2068 
parent 6213  f5bdd6497e08 
child 9548  15bee2731e43 
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 

8812  29 
$(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy Bool.ML Bool.thy \ 
30 
Cardinal.ML Cardinal.thy CardinalArith.ML CardinalArith.thy \ 

31 
Cardinal_AC.ML Cardinal_AC.thy Datatype.ML Datatype.thy Epsilon.ML \ 

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

33 
Inductive.thy InfDatatype.ML InfDatatype.thy Integ/Bin.ML \ 

34 
Integ/Bin.thy Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML \ 

35 
Integ/Int.thy Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy \ 

36 
Main.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML \ 

37 
OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \ 

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

39 
Rel.ML Rel.thy Sum.ML Sum.thy Tools/cartprod.ML \ 

40 
Tools/datatype_package.ML Tools/induct_tacs.ML \ 

41 
Tools/inductive_package.ML Tools/primrec_package.ML Tools/typechk.ML \ 

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

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

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

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

46 
thy_syntax.ML upair.ML upair.thy 

6213  47 
@$(ISATOOL) usedir b r $(OUT)/FOL ZF 
2500  48 

49 

4518  50 
## ZFIMP 
2500  51 

4518  52 
ZFIMP: ZF $(LOG)/ZFIMP.gz 
2500  53 

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

2828  56 
@$(ISATOOL) usedir $(OUT)/ZF IMP 
2500  57 

58 

4518  59 
## ZFCoind 
2500  60 

4518  61 
ZFCoind: ZF $(LOG)/ZFCoind.gz 
2500  62 

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

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

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

67 
Coind/Values.thy 

2828  68 
@$(ISATOOL) usedir $(OUT)/ZF Coind 
2500  69 

70 

4518  71 
## ZFAC 
2500  72 

4518  73 
ZFAC: ZF $(LOG)/ZFAC.gz 
2500  74 

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

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

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

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

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

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

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

5464  83 
AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO7.thy AC/WO1_WO8.ML AC/WO2_AC16.ML \ 
4518  84 
AC/WO2_AC16.thy AC/WO6_WO1.ML AC/WO6_WO1.thy AC/WO_AC.ML AC/WO_AC.thy \ 
85 
AC/recfunAC16.ML AC/recfunAC16.thy AC/rel_is_fun.ML AC/rel_is_fun.thy 

2828  86 
@$(ISATOOL) usedir $(OUT)/ZF AC 
2500  87 

88 

4518  89 
## ZFResid 
90 

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

2500  92 

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

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

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

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

97 
Resid/Substitution.ML \ 
4518  98 
Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy 
2828  99 
@$(ISATOOL) usedir $(OUT)/ZF Resid 
2500  100 

101 

4518  102 
## ZFex 
103 

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

2500  105 

4518  106 
$(LOG)/ZFex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \ 
5539  107 
ex/BinEx.ML ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ 
4518  108 
ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Data.ML ex/Data.thy ex/Enum.ML \ 
5539  109 
ex/Enum.thy ex/LList.ML ex/LList.thy \ 
4518  110 
ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \ 
111 
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

112 
ex/Primrec_defs.ML ex/Primrec_defs.thy \ 
4518  113 
ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \ 
114 
ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \ 

5539  115 
ex/Term.ML ex/Term.thy ex/misc.ML 
2828  116 
@$(ISATOOL) usedir $(OUT)/ZF ex 
2500  117 

118 

4518  119 
## clean 
4447  120 

121 
clean: 

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

124 
$(LOG)/ZFex.gz 