src/HOL/Conditionally_Complete_Lattices.thy

 end
 
 
 text \<open>
 
-To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
-@{const Inf} in theorem names with c.
+To avoid name classes with the \<^class>\<open>complete_lattice\<close>-class we prefix \<^const>\<open>Sup\<close> and
+\<^const>\<open>Inf\<close> in theorem names with c.
 
 \<close>
 
 class conditionally_complete_lattice = lattice + Sup + Inf +
   assumes cInf_lower: "x \<in> X \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X \<le> x"