src/HOL/HoareParallel/RG_Examples.thy
changeset 13601 fd3e3d6b37b2
parent 13517 42efec18f5b2
child 14174 f3cafd2929d5
     1.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Mon Sep 30 16:12:16 2002 +0200
     1.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Mon Sep 30 16:14:02 2002 +0200
     1.3 @@ -149,7 +149,7 @@
     1.4     apply simp
     1.5     apply(subgoal_tac "j=0")
     1.6      apply (rotate_tac -1)
     1.7 -    apply simp
     1.8 +    apply (simp (asm_lr))
     1.9     apply arith
    1.10    apply clarify
    1.11    apply(case_tac i,simp,simp)
    1.12 @@ -340,8 +340,6 @@
    1.13         apply(drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
    1.14          apply assumption+
    1.15         apply simp+
    1.16 -     apply(erule_tac x=j in allE)
    1.17 -     apply force
    1.18      apply clarsimp
    1.19      apply fastsimp
    1.20  apply force+