# HG changeset patch
# User wenzelm
# Date 1360856132 -3600
# Node ID 34dbeb8f16a959f5aa727f6c86b3ec83595f26ed
# Parent  4b3a062b65385ab8b408651a8b9ccaab2c070148
tuned proof;

diff -r 4b3a062b6538 -r 34dbeb8f16a9 src/HOL/Hoare_Parallel/RG_Examples.thy
--- 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