tuned proof;

--- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Thu Feb 14 16:25:13 2013 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Thu Feb 14 16:35:32 2013 +0100
@@ -323,9 +323,8 @@
         (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i)\<rbrace>]"
 apply(rule Parallel)
 --{* 5 subgoals left *}
+apply auto
 apply force+
-apply clarify
-apply simp
 apply(rule While)
     apply force
    apply force