24 ## HOL |
24 ## HOL |
25 |
25 |
26 HOL: |
26 HOL: |
27 @cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL |
27 @cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL |
28 |
28 |
29 styles: |
|
30 @rm -f isabelle.sty |
|
31 @rm -f isabellesym.sty |
|
32 @rm -f pdfsetup.sty |
|
33 @$(ISABELLE_TOOL) latex -o sty >/dev/null |
|
34 @rm -f pdfsetup.sty |
|
35 @rm -f */document/isabelle.sty |
|
36 @rm -f */document/isabellesym.sty |
|
37 @rm -f */document/pdfsetup.sty |
|
38 @rm -f */document/session.tex |
|
39 |
|
40 |
29 |
41 |
30 |
42 ## HOL-Ifexpr |
31 ## HOL-Ifexpr |
43 |
32 |
44 HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz |
33 HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz |
45 |
34 |
46 $(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML |
35 $(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML |
47 $(USEDIR) Ifexpr |
36 $(USEDIR) Ifexpr |
|
37 @rm -f Ifexpr/document/isabelle.sty |
|
38 @rm -f Ifexpr/document/isabellesym.sty |
|
39 @rm -f Ifexpr/document/pdfsetup.sty |
|
40 @rm -f Ifexpr/document/session.tex |
48 @rm -f tutorial.dvi |
41 @rm -f tutorial.dvi |
49 |
42 |
50 ## HOL-ToyList |
43 ## HOL-ToyList |
51 |
44 |
52 HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz |
45 HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz |
54 ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2 |
47 ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2 |
55 cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy |
48 cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy |
56 |
49 |
57 $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML |
50 $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML |
58 $(USEDIR) ToyList2 |
51 $(USEDIR) ToyList2 |
|
52 @rm -f ToyList2/document/isabelle.sty |
|
53 @rm -f ToyList2/document/isabellesym.sty |
|
54 @rm -f ToyList2/document/pdfsetup.sty |
|
55 @rm -f ToyList2/document/session.tex |
59 @rm -f tutorial.dvi |
56 @rm -f tutorial.dvi |
60 |
57 |
61 $(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML |
58 $(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML |
62 $(USEDIR) ToyList |
59 $(USEDIR) ToyList |
|
60 @rm -f ToyList/document/isabelle.sty |
|
61 @rm -f ToyList/document/isabellesym.sty |
|
62 @rm -f ToyList/document/pdfsetup.sty |
|
63 @rm -f ToyList/document/session.tex |
63 @rm -f tutorial.dvi |
64 @rm -f tutorial.dvi |
64 |
65 |
65 ## HOL-CodeGen |
66 ## HOL-CodeGen |
66 |
67 |
67 HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz |
68 HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz |
68 |
69 |
69 $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy |
70 $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy |
70 $(USEDIR) CodeGen |
71 $(USEDIR) CodeGen |
|
72 @rm -f CodeGen/document/isabelle.sty |
|
73 @rm -f CodeGen/document/isabellesym.sty |
|
74 @rm -f CodeGen/document/pdfsetup.sty |
|
75 @rm -f CodeGen/document/session.tex |
71 @rm -f tutorial.dvi |
76 @rm -f tutorial.dvi |
72 |
77 |
73 |
78 |
74 ## HOL-Datatype |
79 ## HOL-Datatype |
75 |
80 |
77 |
82 |
78 $(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \ |
83 $(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \ |
79 Datatype/Nested.thy Datatype/unfoldnested.thy \ |
84 Datatype/Nested.thy Datatype/unfoldnested.thy \ |
80 Datatype/Fundata.thy |
85 Datatype/Fundata.thy |
81 $(USEDIR) Datatype |
86 $(USEDIR) Datatype |
|
87 @rm -f Datatype/document/isabelle.sty |
|
88 @rm -f Datatype/document/isabellesym.sty |
|
89 @rm -f Datatype/document/pdfsetup.sty |
|
90 @rm -f Datatype/document/session.tex |
82 @rm -f tutorial.dvi |
91 @rm -f tutorial.dvi |
83 |
92 |
84 |
93 |
85 ## HOL-Trie |
94 ## HOL-Trie |
86 |
95 |
87 HOL-Trie: HOL $(LOG)/HOL-Trie.gz |
96 HOL-Trie: HOL $(LOG)/HOL-Trie.gz |
88 |
97 |
89 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy |
98 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy |
90 $(USEDIR) Trie |
99 $(USEDIR) Trie |
|
100 @rm -f Trie/document/isabelle.sty |
|
101 @rm -f Trie/document/isabellesym.sty |
|
102 @rm -f Trie/document/pdfsetup.sty |
|
103 @rm -f Trie/document/session.tex |
91 @rm -f tutorial.dvi |
104 @rm -f tutorial.dvi |
92 |
105 |
93 |
106 |
94 ## HOL-Fun |
107 ## HOL-Fun |
95 |
108 |
96 HOL-Fun: HOL $(LOG)/HOL-Fun.gz |
109 HOL-Fun: HOL $(LOG)/HOL-Fun.gz |
97 |
110 |
98 $(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy |
111 $(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy |
99 $(USEDIR) Fun |
112 $(USEDIR) Fun |
|
113 @rm -f Fun/document/isabelle.sty |
|
114 @rm -f Fun/document/isabellesym.sty |
|
115 @rm -f Fun/document/pdfsetup.sty |
|
116 @rm -f Fun/document/session.tex |
100 @rm -f tutorial.dvi |
117 @rm -f tutorial.dvi |
101 |
118 |
102 |
119 |
103 ## HOL-Advanced |
120 ## HOL-Advanced |
104 |
121 |
105 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz |
122 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz |
106 |
123 |
107 $(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML |
124 $(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML |
108 $(USEDIR) Advanced |
125 $(USEDIR) Advanced |
|
126 @rm -f Advanced/document/isabelle.sty |
|
127 @rm -f Advanced/document/isabellesym.sty |
|
128 @rm -f Advanced/document/pdfsetup.sty |
|
129 @rm -f Advanced/document/session.tex |
109 @rm -f tutorial.dvi |
130 @rm -f tutorial.dvi |
110 |
131 |
111 ## HOL-Rules |
132 ## HOL-Rules |
112 |
133 |
113 HOL-Rules: HOL $(LOG)/HOL-Rules.gz |
134 HOL-Rules: HOL $(LOG)/HOL-Rules.gz |
114 |
135 |
115 $(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \ |
136 $(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \ |
116 Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \ |
137 Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \ |
117 Rules/Tacticals.thy Rules/find2.thy Rules/ROOT.ML |
138 Rules/Tacticals.thy Rules/find2.thy Rules/ROOT.ML |
118 @$(USEDIR) Rules |
139 @$(USEDIR) Rules |
|
140 @rm -f Rules/document/isabelle.sty |
|
141 @rm -f Rules/document/isabellesym.sty |
|
142 @rm -f Rules/document/pdfsetup.sty |
|
143 @rm -f Rules/document/session.tex |
119 @rm -f tutorial.dvi |
144 @rm -f tutorial.dvi |
120 |
145 |
121 ## HOL-Sets |
146 ## HOL-Sets |
122 |
147 |
123 HOL-Sets: HOL $(LOG)/HOL-Sets.gz |
148 HOL-Sets: HOL $(LOG)/HOL-Sets.gz |
124 |
149 |
125 $(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \ |
150 $(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \ |
126 Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML |
151 Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML |
127 @$(USEDIR) Sets |
152 @$(USEDIR) Sets |
|
153 @rm -f Sets/document/isabelle.sty |
|
154 @rm -f Sets/document/isabellesym.sty |
|
155 @rm -f Sets/document/pdfsetup.sty |
|
156 @rm -f Sets/document/session.tex |
128 @rm -f tutorial.dvi |
157 @rm -f tutorial.dvi |
129 |
158 |
130 ## HOL-CTL |
159 ## HOL-CTL |
131 |
160 |
132 HOL-CTL: HOL $(LOG)/HOL-CTL.gz |
161 HOL-CTL: HOL $(LOG)/HOL-CTL.gz |
133 |
162 |
134 $(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML |
163 $(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML |
135 $(USEDIR) CTL |
164 $(USEDIR) CTL |
|
165 @rm -f CTL/document/isabelle.sty |
|
166 @rm -f CTL/document/isabellesym.sty |
|
167 @rm -f CTL/document/pdfsetup.sty |
|
168 @rm -f CTL/document/session.tex |
136 @rm -f tutorial.dvi |
169 @rm -f tutorial.dvi |
137 |
170 |
138 ## HOL-Inductive |
171 ## HOL-Inductive |
139 |
172 |
140 HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz |
173 HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz |
141 |
174 |
142 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \ |
175 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \ |
143 Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \ |
176 Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \ |
144 Inductive/Advanced.thy |
177 Inductive/Advanced.thy |
145 $(USEDIR) Inductive |
178 $(USEDIR) Inductive |
|
179 @rm -f Inductive/document/isabelle.sty |
|
180 @rm -f Inductive/document/isabellesym.sty |
|
181 @rm -f Inductive/document/pdfsetup.sty |
|
182 @rm -f Inductive/document/session.tex |
146 @rm -f tutorial.dvi |
183 @rm -f tutorial.dvi |
147 |
184 |
148 ## HOL-Types |
185 ## HOL-Types |
149 |
186 |
150 HOL-Types: HOL $(LOG)/HOL-Types.gz |
187 HOL-Types: HOL $(LOG)/HOL-Types.gz |
151 |
188 |
152 $(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \ |
189 $(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \ |
153 Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \ |
190 Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \ |
154 Types/Overloading.thy Types/Axioms.thy |
191 Types/Overloading.thy Types/Axioms.thy |
155 $(USEDIR) Types |
192 $(USEDIR) Types |
|
193 @rm -f Types/document/isabelle.sty |
|
194 @rm -f Types/document/isabellesym.sty |
|
195 @rm -f Types/document/pdfsetup.sty |
|
196 @rm -f Types/document/session.tex |
156 @rm -f tutorial.dvi |
197 @rm -f tutorial.dvi |
157 |
198 |
158 ## HOL-Misc |
199 ## HOL-Misc |
159 |
200 |
160 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
201 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
173 |
218 |
174 $(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML \ |
219 $(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML \ |
175 Protocol/Message.thy Protocol/Event.thy \ |
220 Protocol/Message.thy Protocol/Event.thy \ |
176 Protocol/Public.thy Protocol/NS_Public.thy |
221 Protocol/Public.thy Protocol/NS_Public.thy |
177 $(USEDIR) Protocol |
222 $(USEDIR) Protocol |
|
223 @rm -f Protocol/document/isabelle.sty |
|
224 @rm -f Protocol/document/isabellesym.sty |
|
225 @rm -f Protocol/document/pdfsetup.sty |
|
226 @rm -f Protocol/document/session.tex |
178 @rm -f tutorial.dvi |
227 @rm -f tutorial.dvi |
179 |
228 |
180 ## HOL-Documents |
229 ## HOL-Documents |
181 |
230 |
182 HOL-Documents: HOL $(LOG)/HOL-Documents.gz |
231 HOL-Documents: HOL $(LOG)/HOL-Documents.gz |
183 |
232 |
184 $(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML |
233 $(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML |
185 $(USEDIR) Documents |
234 $(USEDIR) Documents |
|
235 @rm -f Documents/document/isabelle.sty |
|
236 @rm -f Documents/document/isabellesym.sty |
|
237 @rm -f Documents/document/pdfsetup.sty |
|
238 @rm -f Documents/document/session.tex |
186 @rm -f tutorial.dvi |
239 @rm -f tutorial.dvi |
187 |
240 |
188 ## clean |
241 ## clean |
189 |
242 |
190 clean: |
243 clean: |