--- a/src/HOL/Partial_Function.thy Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Partial_Function.thy Thu Mar 11 07:05:38 2021 +0000
@@ -35,13 +35,13 @@
have "\<Squnion>(insert x A) \<le> \<Squnion>A" using chain
by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain'])
hence "\<Squnion>(insert x A) = \<Squnion>A"
- by(rule antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain'])
+ by(rule order.antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain'])
with \<open>\<Squnion>A \<in> A\<close> show ?thesis by simp
next
case False
with chainD[OF chain, of x "\<Squnion>A"] \<open>\<Squnion>A \<in> A\<close>
have "\<Squnion>(insert x A) = x"
- by(auto intro: antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain])
+ by(auto intro: order.antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain])
thus ?thesis by simp
qed
qed