| changeset 21312 | 1d39091a3208 |
| parent 20432 | 07ec57376051 |
| child 22780 | 41162a270151 |
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Sat Nov 11 23:58:46 2006 +0100 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Sun Nov 12 19:22:10 2006 +0100 @@ -965,7 +965,6 @@ apply (simp only:) apply (rule check_type_mono) apply assumption apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append max_ac) -apply arith apply (simp add: nth_append) apply (erule conjE)+