changeset 51121 | 34dbeb8f16a9 |
parent 44890 | 22f665a2e91c |
child 52567 | b6912471b8f5 |
--- 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