380 Transcendental.thy \ |
380 Transcendental.thy \ |
381 Tools/float_syntax.ML \ |
381 Tools/float_syntax.ML \ |
382 Tools/Qelim/ferrante_rackoff_data.ML \ |
382 Tools/Qelim/ferrante_rackoff_data.ML \ |
383 Tools/Qelim/ferrante_rackoff.ML \ |
383 Tools/Qelim/ferrante_rackoff.ML \ |
384 Tools/Qelim/langford_data.ML \ |
384 Tools/Qelim/langford_data.ML \ |
385 Tools/Qelim/langford.ML |
385 Tools/Qelim/langford.ML \ |
|
386 Tools/SMT/smt_real.ML |
386 |
387 |
387 $(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES) |
388 $(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES) |
388 @$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL |
389 @$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL |
389 |
390 |
390 $(OUT)/HOL-Proofs: ROOT.ML $(HOL_DEPENDENCIES) |
391 $(OUT)/HOL-Proofs: ROOT.ML $(HOL_DEPENDENCIES) |
1189 Library/Numeral_Type.thy Word/Num_Lemmas.thy Word/TdThs.thy \ |
1190 Library/Numeral_Type.thy Word/Num_Lemmas.thy Word/TdThs.thy \ |
1190 Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy \ |
1191 Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy \ |
1191 Word/BinBoolList.thy Word/BitSyntax.thy Word/WordDefinition.thy \ |
1192 Word/BinBoolList.thy Word/BitSyntax.thy Word/WordDefinition.thy \ |
1192 Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy \ |
1193 Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy \ |
1193 Word/WordGenLib.thy Word/Word.thy Word/document/root.tex \ |
1194 Word/WordGenLib.thy Word/Word.thy Word/document/root.tex \ |
1194 Word/document/root.bib |
1195 Word/document/root.bib Tools/SMT/smt_word.ML |
1195 @cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word |
1196 @cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word |
1196 |
1197 |
1197 |
1198 |
1198 ## HOL-Word-Examples |
1199 ## HOL-Word-Examples |
1199 |
1200 |
1253 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle |
1254 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle |
1254 |
1255 |
1255 |
1256 |
1256 ## HOL-SMT_Examples |
1257 ## HOL-SMT_Examples |
1257 |
1258 |
1258 HOL-SMT_Examples: HOL $(LOG)/HOL-SMT_Examples.gz |
1259 HOL-SMT_Examples: HOL-Word $(LOG)/HOL-SMT_Examples.gz |
1259 |
1260 |
1260 $(LOG)/HOL-SMT_Examples.gz: $(OUT)/HOL-SMT SMT_Examples/ROOT.ML \ |
1261 $(LOG)/HOL-SMT_Examples.gz: $(OUT)/HOL-SMT SMT_Examples/ROOT.ML \ |
1261 SMT_Examples/SMT_Examples.thy SMT_Examples/SMT_Examples.certs |
1262 SMT_Examples/SMT_Examples.thy SMT_Examples/SMT_Examples.certs \ |
1262 @cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL Examples |
1263 SMT_Examples/SMT_Word_Examples.thy SMT_Examples/SMT_Tests.thy \ |
|
1264 SMT_Examples/SMT_Word_Examples.certs SMT_Examples/SMT_Tests.certs |
|
1265 @$(ISABELLE_TOOL) usedir $(OUT)/HOL-Word SMT_Examples |
1263 |
1266 |
1264 |
1267 |
1265 ## HOL-Boogie |
1268 ## HOL-Boogie |
1266 |
1269 |
1267 HOL-Boogie: HOL $(OUT)/HOL-Boogie |
1270 HOL-Boogie: HOL-Word $(OUT)/HOL-Boogie |
1268 |
1271 |
1269 $(OUT)/HOL-Boogie: $(OUT)/HOL Boogie/ROOT.ML Boogie/Boogie.thy \ |
1272 $(OUT)/HOL-Boogie: $(OUT)/HOL Boogie/ROOT.ML Boogie/Boogie.thy \ |
1270 Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML \ |
1273 Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML \ |
1271 Boogie/Tools/boogie_commands.ML Boogie/Tools/boogie_tactics.ML |
1274 Boogie/Tools/boogie_commands.ML Boogie/Tools/boogie_tactics.ML |
1272 @cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Boogie |
1275 @cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-Boogie |
1273 |
1276 |
1274 |
1277 |
1275 ## HOL-Boogie_Examples |
1278 ## HOL-Boogie_Examples |
1276 |
1279 |
1277 HOL-Boogie-Examples: HOL-Boogie $(LOG)/HOL-Boogie-Examples.gz |
1280 HOL-Boogie-Examples: HOL-Boogie $(LOG)/HOL-Boogie-Examples.gz |