292 MiniML/Maybe.ML MiniML/Maybe.thy MiniML/MiniML.ML MiniML/MiniML.thy \ |
292 MiniML/Maybe.ML MiniML/Maybe.thy MiniML/MiniML.ML MiniML/MiniML.thy \ |
293 MiniML/ROOT.ML MiniML/Type.ML MiniML/Type.thy MiniML/W.ML MiniML/W.thy |
293 MiniML/ROOT.ML MiniML/Type.ML MiniML/Type.thy MiniML/W.ML MiniML/W.thy |
294 @$(ISATOOL) usedir $(OUT)/HOL MiniML |
294 @$(ISATOOL) usedir $(OUT)/HOL MiniML |
295 |
295 |
296 |
296 |
|
297 ## HOL-MicroJava |
|
298 |
|
299 HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz |
|
300 |
|
301 $(LOG)/HOL-MicroJava.gz: $(OUT)/HOL \ |
|
302 MicroJava/J/Conform.ML MicroJava/J/Conform.thy MicroJava/J/Decl.thy \ |
|
303 MicroJava/J/Eval.thy MicroJava/J/Eval.ML MicroJava/J/JBasis.ML \ |
|
304 MicroJava/J/JBasis.thy MicroJava/J/JTypeSafe.thy MicroJava/J/JTypeSafe.ML \ |
|
305 MicroJava/J/Prog.thy MicroJava/J/Prog.ML MicroJava/J/State.ML \ |
|
306 MicroJava/J/State.thy MicroJava/J/Term.thy MicroJava/J/Type.ML \ |
|
307 MicroJava/J/Type.thy MicroJava/J/TypeRel.ML MicroJava/J/TypeRel.thy \ |
|
308 MicroJava/J/WellForm.thy MicroJava/J/WellForm.ML \ |
|
309 MicroJava/J/WellType.ML MicroJava/J/WellType.thy \ |
|
310 MicroJava/JVM/Control.thy MicroJava/JVM/JVMExec.thy \ |
|
311 MicroJava/JVM/JVMState.thy MicroJava/JVM/LoadAndStore.thy \ |
|
312 MicroJava/JVM/Method.thy MicroJava/JVM/Method.ML \ |
|
313 MicroJava/JVM/Object.thy MicroJava/JVM/Opstack.thy \ |
|
314 MicroJava/JVM/Store.thy MicroJava/JVM/Store.ML \ |
|
315 MicroJava/BV/BVSpec.thy MicroJava/BV/BVSpec.ML \ |
|
316 MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/BVSpecTypeSafe.ML \ |
|
317 MicroJava/BV/Convert.thy MicroJava/BV/Convert.ML \ |
|
318 MicroJava/BV/Correct.thy MicroJava/BV/Correct.ML |
|
319 @$(ISATOOL) usedir $(OUT)/HOL MicroJava |
|
320 |
297 ## HOL-BCV |
321 ## HOL-BCV |
298 |
322 |
299 HOL-BCV: HOL $(LOG)/HOL-BCV.gz |
323 HOL-BCV: HOL $(LOG)/HOL-BCV.gz |
300 |
324 |
301 $(LOG)/HOL-BCV.gz: $(OUT)/HOL BCV/DFAandWTI.ML \ |
325 $(LOG)/HOL-BCV.gz: $(OUT)/HOL BCV/DFAandWTI.ML \ |