Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hoare_Parallel/RG_Examples.thy
changeset 69768 7e4966eaf781
parent 69546 27dae626822b 
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Thu Jan 31 09:30:15 2019 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Thu Jan 31 13:08:59 2019 +0000
@@ -320,8 +320,8 @@
       \<lbrace>True\<rbrace>,
       \<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>
         (\<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)
-apply (auto cong del: INF_cong_simp SUP_cong_simp)
+  apply (rule Parallel)
+apply (auto cong del: image_cong_simp)
 apply force
 apply (rule While)
     apply force
isabelle