src/HOL/Hoare_Parallel/OG_Examples.thy
changeset 60149 9b0825a00b1a
parent 59189 ad8e0a789af6
child 60151 9023d59acce6
equal deleted inserted replaced
60148:f0fc2378a479 60149:9b0825a00b1a
   190 apply force
   190 apply force
   191 apply force
   191 apply force
   192 --\<open>6 subgoals left\<close>
   192 --\<open>6 subgoals left\<close>
   193 prefer 6
   193 prefer 6
   194 apply(erule_tac x=i in allE)
   194 apply(erule_tac x=i in allE)
       
   195 apply simp
   195 apply fastforce
   196 apply fastforce
   196 --\<open>5 subgoals left\<close>
   197 --\<open>5 subgoals left\<close>
   197 prefer 5
   198 prefer 5
   198 apply(case_tac [!] "j=k")
   199 apply(case_tac [!] "j=k")
   199 --\<open>10 subgoals left\<close>
   200 --\<open>10 subgoals left\<close>