327 ## HOL-MicroJava |
327 ## HOL-MicroJava |
328 |
328 |
329 HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz |
329 HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz |
330 |
330 |
331 $(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \ |
331 $(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \ |
332 MicroJava/J/Conform.ML MicroJava/J/Conform.thy MicroJava/J/Decl.thy \ |
332 MicroJava/J/Conform.ML MicroJava/J/Conform.thy \ |
333 MicroJava/J/Eval.thy MicroJava/J/Eval.ML MicroJava/J/JBasis.ML \ |
333 MicroJava/J/Eval.thy MicroJava/J/Eval.ML MicroJava/J/JBasis.ML \ |
334 MicroJava/J/JBasis.thy MicroJava/J/JTypeSafe.thy MicroJava/J/JTypeSafe.ML \ |
334 MicroJava/J/JBasis.thy MicroJava/J/JTypeSafe.thy MicroJava/J/JTypeSafe.ML \ |
335 MicroJava/J/Prog.thy MicroJava/J/Prog.ML MicroJava/J/State.ML \ |
335 MicroJava/J/Decl.thy MicroJava/J/Decl.ML MicroJava/J/State.ML \ |
336 MicroJava/J/State.thy MicroJava/J/Term.thy MicroJava/J/Type.ML \ |
336 MicroJava/J/State.thy MicroJava/J/Term.thy \ |
337 MicroJava/J/Type.thy MicroJava/J/TypeRel.ML MicroJava/J/TypeRel.thy \ |
337 MicroJava/J/Type.thy MicroJava/J/TypeRel.ML MicroJava/J/TypeRel.thy \ |
338 MicroJava/J/WellForm.thy MicroJava/J/WellForm.ML \ |
338 MicroJava/J/WellForm.thy MicroJava/J/WellForm.ML MicroJava/J/Value.thy \ |
339 MicroJava/J/WellType.ML MicroJava/J/WellType.thy \ |
339 MicroJava/J/WellType.ML MicroJava/J/WellType.thy \ |
|
340 MicroJava/J/Example.ML MicroJava/J/Example.thy \ |
340 MicroJava/JVM/Control.thy MicroJava/JVM/JVMExec.thy \ |
341 MicroJava/JVM/Control.thy MicroJava/JVM/JVMExec.thy \ |
341 MicroJava/JVM/JVMState.thy MicroJava/JVM/LoadAndStore.thy \ |
342 MicroJava/JVM/JVMState.thy MicroJava/JVM/LoadAndStore.thy \ |
342 MicroJava/JVM/Method.thy MicroJava/JVM/Object.thy MicroJava/JVM/Opstack.thy \ |
343 MicroJava/JVM/Method.thy MicroJava/JVM/Object.thy MicroJava/JVM/Opstack.thy \ |
343 MicroJava/JVM/Store.thy MicroJava/JVM/Store.ML \ |
344 MicroJava/JVM/Store.thy MicroJava/JVM/Store.ML \ |
344 MicroJava/BV/BVSpec.thy MicroJava/BV/BVSpec.ML \ |
345 MicroJava/BV/BVSpec.thy MicroJava/BV/BVSpec.ML \ |