src/HOL/HoareParallel/RG_Examples.thy

    apply(erule disjE)
     apply clarify
     apply simp
    apply clarify
    apply simp
-   apply(case_tac j,simp,simp)
+   apply(subgoal_tac "j=0")
+    apply (rotate_tac -1)
+    apply simp
+   apply arith
   apply clarify
   apply(case_tac i,simp,simp)
  apply clarify   
  apply simp
  apply(erule_tac x=0 in all_dupE)

     apply(rule subset_refl)+
  apply(rule Cond)
     apply force
    apply(rule Basic)
       apply force
-     apply force
+     apply fastsimp
     apply force
    apply force
   apply(rule Basic)
      apply simp
      apply clarify

         apply assumption+
        apply simp+
      apply(erule_tac x=j in allE)
      apply force
     apply clarsimp
-    apply force
+    apply fastsimp
 apply force+
 done
 
 text {* Same but with a list as auxiliary variable: *}