diff -r 7a4baad05495 -r 16a26996c30e src/HOL/HoareParallel/RG_Examples.thy
--- a/src/HOL/HoareParallel/RG_Examples.thy	Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy	Fri Jul 18 18:25:53 2008 +0200
@@ -1,6 +1,8 @@
 header {* \section{Examples} *}
 
-theory RG_Examples imports RG_Syntax begin
+theory RG_Examples
+imports RG_Syntax
+begin
 
 lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def 
 
@@ -291,18 +293,14 @@
     apply force
    apply force
   apply(rule Basic)
-     apply simp
+     apply (simp add: mod_add_self2)
      apply clarify
      apply simp
-     apply(case_tac "X x (j mod n)\<le> j")
-      apply(drule le_imp_less_or_eq)
-      apply(erule disjE)
-       apply(drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
-        apply assumption+
-       apply simp+
-    apply clarsimp
-    apply fastsimp
-apply force+
+     apply (case_tac "X x (j mod n) \<le> j")
+     apply (drule le_imp_less_or_eq)
+     apply (erule disjE)
+     apply (drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
+     apply auto
 done
 
 text {* Same but with a list as auxiliary variable: *}
@@ -348,16 +346,14 @@
   apply(rule Basic)
      apply simp
      apply clarify
-     apply simp
+     apply (simp add: mod_add_self2)
      apply(rule allI)
      apply(rule impI)+
      apply(case_tac "X x ! i\<le> j")
       apply(drule le_imp_less_or_eq)
       apply(erule disjE)
        apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux)
-        apply assumption+
-       apply simp
-apply force+
+     apply auto
 done
 
 end