--- a/src/HOL/Hoare_Parallel/OG_Examples.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Sun Oct 21 09:39:09 2018 +0200
@@ -534,9 +534,9 @@
COEND
\<lbrace>\<acute>x=n\<rbrace>"
apply oghoare
-apply (simp_all cong del: sum.strong_cong)
+apply (simp_all cong del: sum.cong_strong)
apply (tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
-apply (simp_all cong del: sum.strong_cong)
+apply (simp_all cong del: sum.cong_strong)
apply(erule (1) Example2_lemma2)
apply(erule (1) Example2_lemma2)
apply(erule (1) Example2_lemma2)