equal
deleted
inserted
replaced
485 ## HOL-MicroJava |
485 ## HOL-MicroJava |
486 |
486 |
487 HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz |
487 HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz |
488 |
488 |
489 $(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \ |
489 $(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \ |
|
490 MicroJava/Comp/AuxLemmas.thy \ |
|
491 MicroJava/Comp/CorrComp.thy \ |
|
492 MicroJava/Comp/CorrCompTp.thy \ |
|
493 MicroJava/Comp/DefsComp.thy \ |
|
494 MicroJava/Comp/Index.thy \ |
|
495 MicroJava/Comp/LemmasComp.thy \ |
|
496 MicroJava/Comp/NatCanonify.thy \ |
|
497 MicroJava/Comp/TranslComp.thy \ |
|
498 MicroJava/Comp/TranslCompTp.thy \ |
|
499 MicroJava/Comp/TypeInf.thy \ |
490 MicroJava/J/Conform.thy MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \ |
500 MicroJava/J/Conform.thy MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \ |
491 MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \ |
501 MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \ |
492 MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \ |
502 MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \ |
493 MicroJava/J/WellForm.thy MicroJava/J/Value.thy \ |
503 MicroJava/J/WellForm.thy MicroJava/J/Value.thy \ |
494 MicroJava/J/WellType.thy MicroJava/J/Example.thy \ |
504 MicroJava/J/WellType.thy MicroJava/J/Example.thy \ |