equal
deleted
inserted
replaced
5 ## targets |
5 ## targets |
6 |
6 |
7 default: HOLCF |
7 default: HOLCF |
8 images: HOLCF IOA |
8 images: HOLCF IOA |
9 test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \ |
9 test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \ |
|
10 HOLCF-Tutorial \ |
10 IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex |
11 IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex |
11 all: images test |
12 all: images test |
12 |
13 |
13 |
14 |
14 ## global settings |
15 ## global settings |
76 Tools/repdef.ML \ |
77 Tools/repdef.ML \ |
77 document/root.tex |
78 document/root.tex |
78 @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF |
79 @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF |
79 |
80 |
80 |
81 |
|
82 ## HOLCF-Tutorial |
|
83 |
|
84 HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz |
|
85 |
|
86 $(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \ |
|
87 Tutorial/Domain_ex.thy \ |
|
88 Tutorial/Fixrec_ex.thy \ |
|
89 Tutorial/New_Domain.thy \ |
|
90 Tutorial/document/root.tex \ |
|
91 Tutorial/ROOT.ML |
|
92 @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial |
|
93 |
|
94 |
81 ## HOLCF-IMP |
95 ## HOLCF-IMP |
82 |
96 |
83 HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz |
97 HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz |
84 |
98 |
85 $(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \ |
99 $(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \ |
93 |
107 |
94 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \ |
108 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \ |
95 ../HOL/Library/Nat_Infinity.thy \ |
109 ../HOL/Library/Nat_Infinity.thy \ |
96 ex/Dagstuhl.thy \ |
110 ex/Dagstuhl.thy \ |
97 ex/Dnat.thy \ |
111 ex/Dnat.thy \ |
98 ex/Domain_ex.thy \ |
|
99 ex/Domain_Proofs.thy \ |
112 ex/Domain_Proofs.thy \ |
100 ex/Fix2.thy \ |
113 ex/Fix2.thy \ |
101 ex/Fixrec_ex.thy \ |
|
102 ex/Focus_ex.thy \ |
114 ex/Focus_ex.thy \ |
103 ex/Hoare.thy \ |
115 ex/Hoare.thy \ |
104 ex/Letrec.thy \ |
116 ex/Letrec.thy \ |
105 ex/Loop.thy \ |
117 ex/Loop.thy \ |
106 ex/New_Domain.thy \ |
|
107 ex/Powerdomain_ex.thy \ |
118 ex/Powerdomain_ex.thy \ |
108 ex/Stream.thy \ |
119 ex/Stream.thy \ |
109 ex/Strict_Fun.thy \ |
120 ex/Strict_Fun.thy \ |
110 ex/ROOT.ML |
121 ex/ROOT.ML |
111 @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex |
122 @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex |
199 clean: |
210 clean: |
200 @rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \ |
211 @rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \ |
201 $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \ |
212 $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \ |
202 $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \ |
213 $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \ |
203 $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz \ |
214 $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz \ |
204 $(LOG)/IOA-ex.gz |
215 $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz |