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