src/HOL/Library/Complete_Partial_Order2.thy
changeset 69164 74f1b0f10b2b
parent 69039 51005671bee5
child 69546 27dae626822b
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Sun Oct 21 09:39:09 2018 +0200
@@ -188,7 +188,7 @@
 proof(cases "Y = {}")
   case True
   then show ?thesis
-    by (simp add: image_constant_conv cong del: strong_SUP_cong)
+    by (simp add: image_constant_conv cong del: SUP_cong_strong)
 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: strong_SUP_cong)
+by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_strong)
 
 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.strong_SUP_cong)
+      by (auto simp add: image_constant_conv cong del: c.SUP_cong_strong)
   next
     case False
     let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"