| changeset 16417 | 9bc16273c2d4 |
| parent 14981 | e73f8140af78 |
| child 22271 | 51a80e238b29 |
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Fri Jun 17 16:12:49 2005 +0200 @@ -5,7 +5,7 @@ (* Lemmas for compiler correctness proof *) -theory LemmasComp = TranslComp: +theory LemmasComp imports TranslComp begin declare split_paired_All [simp del]