| changeset 13630 | a013a9dd370f |
| parent 13095 | 8ed413a57bdc |
| child 13675 | 01fc1fc61384 |
--- a/src/HOL/IMP/Compiler.thy Mon Oct 07 19:01:51 2002 +0200 +++ b/src/HOL/IMP/Compiler.thy Tue Oct 08 08:20:17 2002 +0200 @@ -97,10 +97,8 @@ apply(rule iffI) defer apply simp apply(subgoal_tac "n \<le> size p1") - apply(rotate_tac -1) apply simp apply(rule ccontr) -apply(rotate_tac -1) apply(drule_tac f = length in arg_cong) apply simp apply arith