diff -r 6c9453ec2191 -r 74f1b0f10b2b src/HOL/Hoare_Parallel/OG_Examples.thy --- 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 \\x=n\" apply oghoare -apply (simp_all cong del: sum.strong_cong) +apply (simp_all cong del: sum.cong_strong) apply (tactic \ALLGOALS (clarify_tac @{context})\) -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)