src/HOL/Library/Complete_Partial_Order2.thy
changeset 69546 27dae626822b
parent 69164 74f1b0f10b2b
child 69593 3dda49e08b9d
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Sun Dec 30 10:34:56 2018 +0000
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Sun Dec 30 10:34:56 2018 +0000
@@ -188,7 +188,7 @@
 proof(cases "Y = {}")
   case True
   then show ?thesis
-    by (simp add: image_constant_conv cong del: SUP_cong_strong)
+    by (simp add: image_constant_conv cong del: SUP_cong_simp)
 next
   case False
   have chain1: "\<And>f. f \<in> Z \<Longrightarrow> Complete_Partial_Order.chain (\<le>) (f ` Y)"
@@ -518,7 +518,7 @@
 context ccpo begin
 
 lemma cont_const [simp, cont_intro]: "cont luba orda Sup (\<le>) (\<lambda>x. c)"
-by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_strong)
+by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_simp)
 
 lemma mcont_const [cont_intro, simp]:
   "mcont luba orda Sup (\<le>) (\<lambda>x. c)"
@@ -695,7 +695,7 @@
     hence "\<Squnion>Y \<le> bound" using chain by(auto intro: ccpo_Sup_least)
     moreover have "Y \<inter> {x. \<not> x \<le> bound} = {}" using True by auto
     ultimately show ?thesis using True Y
-      by (auto simp add: image_constant_conv cong del: c.SUP_cong_strong)
+      by (auto simp add: image_constant_conv cong del: c.SUP_cong_simp)
   next
     case False
     let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"