src/HOL/HoareParallel/RG_Examples.thy
 changeset 13099 4bb592cdde0e parent 13020 791e3b4c4039 child 13103 66659a4b16f6
```     1.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Mon Apr 29 11:30:15 2002 +0200
1.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Mon Apr 29 16:45:12 2002 +0200
1.3 @@ -310,7 +310,7 @@
1.4    \<lbrace>\<forall>i<n. (\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and>
1.5      (\<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>]"
1.6  apply(rule Parallel)
1.7 -(*5*)
1.8 +--{*5 subgoals left *}
1.9  apply force+
1.10  apply clarify
1.11  apply simp
1.12 @@ -372,7 +372,7 @@
1.13        \<lbrace>\<forall>i<n. (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and>
1.14          (\<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>]"
1.15  apply(rule Parallel)
1.16 -(*5*)
1.17 +--{* 5 subgoals left *}
1.18  apply force+
1.19  apply clarify
1.20  apply simp
```