| changeset 65538 | a39ef48fbee0 |
| parent 60304 | 3f429b7d8eb5 |
| child 67613 | ce654b0e6d69 |
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Fri Apr 21 16:48:12 2017 +0200 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy Fri Apr 21 16:48:58 2017 +0200 @@ -5,7 +5,7 @@ (* Compiler correctness statement and proof *) theory CorrComp -imports "../J/JTypeSafe" "LemmasComp" +imports "../J/JTypeSafe" LemmasComp begin declare wf_prog_ws_prog [simp add]