| changeset 24699 | c6674504103f |
| parent 24074 | 40f414b87655 |
| child 28524 | 644b62cf678f |
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy Tue Sep 25 12:16:08 2007 +0200 @@ -118,7 +118,7 @@ apply (rule exec_all_trans) apply (simp only: append_Nil) apply (drule_tac x="[]" in spec) -apply (simp only: list.simps) +apply (simp only: list.simps list.size) apply blast apply (rule exec_instr_in_exec_all) apply auto