src/HOL/Lattices.thy

   show "x \<nabla> y \<le> x \<squnion> y"
     by (rule leI) simp_all
 qed
 
 
-subsection \<open>Lattice on @{typ bool}\<close>
+subsection \<open>Lattice on \<^typ>\<open>bool\<close>\<close>
 
 instantiation bool :: boolean_algebra
 begin
 
 definition bool_Compl_def [simp]: "uminus = Not"

 
 lemma sup_boolE: "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   by auto
 
 
-subsection \<open>Lattice on @{typ "_ \<Rightarrow> _"}\<close>
+subsection \<open>Lattice on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close>
 
 instantiation "fun" :: (type, semilattice_sup) semilattice_sup
 begin
 
 definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"