src/HOL/Library/Order_Continuity.thy

 proof safe
   fix M :: "nat \<Rightarrow> 'c"
   assume M: "mono M"
   then have "mono (\<lambda>i. g (M i))"
     using sup_continuous_mono[OF g] by (auto simp: mono_def)
-  with M show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
+  with M show "f (g (Sup (M ` UNIV))) = (SUP i. f (g (M i)))"
     by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
 qed
 
 lemma sup_continuous_sup[order_continuous_intros]:
   "sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. sup (f x) (g x))"

 proof safe
   fix M :: "nat \<Rightarrow> 'c"
   assume M: "antimono M"
   then have "antimono (\<lambda>i. g (M i))"
     using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
-  with M show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
+  with M show "f (g (Inf (M ` UNIV))) = (INF i. f (g (M i)))"
     by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
 qed
 
 lemma inf_continuous_gfp:
   assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")