src/HOL/Conditionally_Complete_Lattices.thy

   by (auto intro!: cSup_upper2[of "SOME a. a \<in> A"] intro: someI cInf_lower)
 
 end
 
 instance complete_lattice \<subseteq> conditionally_complete_lattice
-  by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
+  by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
 
 lemma cSup_eq:
   fixes a :: "'a :: {conditionally_complete_lattice, no_bot}"
   assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
   assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"