src/HOL/Library/Complete_Partial_Order2.thy

 qed
 
 lemma mcont_SUP [cont_intro, simp]:
   "\<lbrakk> mcont lub ord Union op \<subseteq> f; \<And>y. mcont lub ord Sup op \<le> (\<lambda>x. g x y) \<rbrakk>
   \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. \<Squnion>y\<in>f x. g x y)"
-by(blast intro: mcontI cont_SUP[OF assms] monotone_SUP mcont_mono)
+by(blast intro: mcontI cont_SUP monotone_SUP mcont_mono)
 
 end
 
 lemma admissible_Ball [cont_intro, simp]:
   "\<lbrakk> \<And>x. ccpo.admissible lub ord (\<lambda>A. P A x);