author  huffman 
Wed, 19 May 2010 17:01:07 0700  
changeset 37000  41a22e7c1145 
parent 35932  86559356502d 
child 37109  e67760c1b851 
permissions  rwrr 
2494  1 
# 
2 
# IsaMakefile for HOLCF 

3 
# 

4 

4518  5 
## targets 
2494  6 

4518  7 
default: HOLCF 
8 
images: HOLCF IOA 

11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset

9 
test: HOLCFIMP HOLCFex HOLCFFOCUS \ 
37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

10 
HOLCFTutorial \ 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset

11 
IOAABP IOANTP IOAModelcheck IOAStorage IOAex 
4518  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 
2494  20 

4518  21 

22 
## HOLCF 

23 

24 
HOLCF: HOL $(OUT)/HOLCF 

25 

26 
HOL: 

28500  27 
@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL 
2494  28 

27420  29 
$(OUT)/HOLCF: $(OUT)/HOL \ 
30 
ROOT.ML \ 

31 
Adm.thy \ 

32 
Algebraic.thy \ 

33 
Bifinite.thy \ 

34 
Cfun.thy \ 

35 
CompactBasis.thy \ 

36 
Completion.thy \ 

37 
Cont.thy \ 

38 
ConvexPD.thy \ 

39 
Cprod.thy \ 

40 
Discrete.thy \ 

41 
Deflation.thy \ 

42 
Domain.thy \ 

35652
05ca920cd94b
move takeproofs stuff into new theory Domain_Aux.thy
huffman
parents:
35530
diff
changeset

43 
Domain_Aux.thy \ 
27420  44 
Eventual.thy \ 
45 
Ffun.thy \ 

46 
Fixrec.thy \ 

47 
Fix.thy \ 

48 
HOLCF.thy \ 

49 
Lift.thy \ 

50 
LowerPD.thy \ 

51 
One.thy \ 

52 
Pcpodef.thy \ 

53 
Pcpo.thy \ 

54 
Porder.thy \ 

35473  55 
Powerdomains.thy \ 
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29130
diff
changeset

56 
Product_Cpo.thy \ 
33783  57 
Representable.thy \ 
27420  58 
Sprod.thy \ 
59 
Ssum.thy \ 

29534  60 
Sum_Cpo.thy \ 
27420  61 
Tr.thy \ 
62 
Universal.thy \ 

63 
UpperPD.thy \ 

64 
Up.thy \ 

65 
Tools/cont_consts.ML \ 

66 
Tools/cont_proc.ML \ 

35475
979019ab92eb
move common functions into new file holcf_library.ML
huffman
parents:
35473
diff
changeset

67 
Tools/holcf_library.ML \ 
32126  68 
Tools/Domain/domain_extender.ML \ 
69 
Tools/Domain/domain_axioms.ML \ 

35473  70 
Tools/Domain/domain_constructors.ML \ 
33795  71 
Tools/Domain/domain_isomorphism.ML \ 
32126  72 
Tools/Domain/domain_library.ML \ 
35530  73 
Tools/Domain/domain_take_proofs.ML \ 
32126  74 
Tools/Domain/domain_theorems.ML \ 
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30920
diff
changeset

75 
Tools/fixrec.ML \ 
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30920
diff
changeset

76 
Tools/pcpodef.ML \ 
33783  77 
Tools/repdef.ML \ 
27420  78 
document/root.tex 
28500  79 
@$(ISABELLE_TOOL) usedir b g true r $(OUT)/HOL HOLCF 
2494  80 

4518  81 

37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

82 
## HOLCFTutorial 
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

83 

41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

84 
HOLCFTutorial: HOLCF $(LOG)/HOLCFTutorial.gz 
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

85 

41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

86 
$(LOG)/HOLCFTutorial.gz: $(OUT)/HOLCF \ 
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

87 
Tutorial/Domain_ex.thy \ 
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

88 
Tutorial/Fixrec_ex.thy \ 
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

89 
Tutorial/New_Domain.thy \ 
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

90 
Tutorial/document/root.tex \ 
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

91 
Tutorial/ROOT.ML 
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

92 
@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial 
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

93 

41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

94 

4518  95 
## HOLCFIMP 
2494  96 

4518  97 
HOLCFIMP: HOLCF $(LOG)/HOLCFIMP.gz 
98 

12433  99 
$(LOG)/HOLCFIMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \ 
12599  100 
IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex 
28500  101 
@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP 
2494  102 

103 

4518  104 
## HOLCFex 
105 

106 
HOLCFex: HOLCF $(LOG)/HOLCFex.gz 

2494  107 

30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset

108 
$(LOG)/HOLCFex.gz: $(OUT)/HOLCF \ 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset

109 
../HOL/Library/Nat_Infinity.thy \ 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset

110 
ex/Dagstuhl.thy \ 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset

111 
ex/Dnat.thy \ 
35167  112 
ex/Domain_Proofs.thy \ 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset

113 
ex/Fix2.thy \ 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset

114 
ex/Focus_ex.thy \ 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset

115 
ex/Hoare.thy \ 
35932
86559356502d
move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
35908
diff
changeset

116 
ex/Letrec.thy \ 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset

117 
ex/Loop.thy \ 
29992  118 
ex/Powerdomain_ex.thy \ 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset

119 
ex/Stream.thy \ 
35167  120 
ex/Strict_Fun.thy \ 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset

121 
ex/ROOT.ML 
28500  122 
@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex 
3081  123 

124 

11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset

125 
## HOLCFFOCUS 
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset

126 

4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset

127 
HOLCFFOCUS: HOLCF $(LOG)/HOLCFFOCUS.gz 
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset

128 

35214  129 
$(LOG)/HOLCFFOCUS.gz: $(OUT)/HOLCF \ 
130 
ex/Stream.thy \ 

131 
FOCUS/Fstreams.thy \ 

19759  132 
FOCUS/Fstream.thy FOCUS/FOCUS.thy \ 
133 
FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \ 

134 
FOCUS/Buffer.thy FOCUS/Buffer_adm.thy 

28500  135 
@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset

136 

4518  137 
## IOA 
138 

139 
IOA: HOLCF $(OUT)/IOA 

140 

19741  141 
$(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \ 
142 
IOA/meta_theory/Asig.thy IOA/meta_theory/CompoScheds.thy \ 

143 
IOA/meta_theory/CompoTraces.thy IOA/meta_theory/Seq.thy \ 

144 
IOA/meta_theory/RefCorrectness.thy IOA/meta_theory/Automata.thy \ 

145 
IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/IOA.thy \ 

146 
IOA/meta_theory/Sequence.thy IOA/meta_theory/CompoExecs.thy \ 

147 
IOA/meta_theory/RefMappings.thy IOA/meta_theory/Compositionality.thy \ 

148 
IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \ 

149 
IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \ 

150 
IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \ 

31773  151 
IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/automaton.ML 
28500  152 
@cd IOA; $(ISABELLE_TOOL) usedir b $(OUT)/HOLCF IOA 
3081  153 

154 

4518  155 
## IOAABP 
156 

157 
IOAABP: IOA $(LOG)/IOAABP.gz 

3081  158 

4518  159 
$(LOG)/IOAABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \ 
8602
f077613e8e7b
mods because of weak_case_cong > removed Action.ML twice
nipkow
parents:
6475
diff
changeset

160 
IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.thy \ 
19738  161 
IOA/ABP/Check.ML IOA/ABP/Correctness.thy \ 
4518  162 
IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \ 
19738  163 
IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ 
4518  164 
IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \ 
165 
IOA/ABP/Spec.thy 

28500  166 
@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP 
3081  167 

4518  168 
## IOANTP 
169 

170 
IOANTP: IOA $(LOG)/IOANTP.gz 

171 

19739  172 
$(LOG)/IOANTP.gz: $(OUT)/IOA \ 
173 
IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \ 

174 
IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \ 

175 
IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \ 

4518  176 
IOA/NTP/Spec.thy 
28500  177 
@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP 
3081  178 

3951  179 

6475  180 
## IOAModelcheck 
181 

182 
IOAModelcheck: IOA $(LOG)/IOAModelcheck.gz 

183 

19764  184 
$(LOG)/IOAModelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \ 
22819  185 
IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.thy \ 
186 
IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy 

28500  187 
@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Modelcheck 
6475  188 

189 

6010  190 
## IOAStorage 
191 

192 
IOAStorage: IOA $(LOG)/IOAStorage.gz 

193 

19740  194 
$(LOG)/IOAStorage.gz: $(OUT)/IOA IOA/Storage/Action.thy \ 
17238
b1cf9189104e
removed IOA/Storage/Impl.ML, IOA/Storage/Action.ML;
wenzelm
parents:
16698
diff
changeset

195 
IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \ 
6011  196 
IOA/Storage/ROOT.ML IOA/Storage/Spec.thy 
28500  197 
@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage 
6010  198 

199 

6475  200 
## IOAex 
201 

202 
IOAex: IOA $(LOG)/IOAex.gz 

203 

19740  204 
$(LOG)/IOAex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy 
28500  205 
@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex 
6475  206 

207 

4518  208 
## clean 
4447  209 

210 
clean: 

33450  211 
@rm f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCFIMP.gz \ 
212 
$(LOG)/HOLCFex.gz $(LOG)/HOLCFFOCUS.gz $(OUT)/IOA \ 

213 
$(LOG)/IOA.gz $(LOG)/IOAABP.gz $(LOG)/IOANTP.gz \ 

214 
$(LOG)/IOAModelcheck.gz $(LOG)/IOAStorage.gz \ 

37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset

215 
$(LOG)/IOAex.gz $(LOG)/HOLCFTutorial.gz 