src/HOL/HOLCF/Tr.thy

 default_sort pcpo
 
 definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a"
   where "tr_case = (\<Lambda> t e (Def b). if b then t else e)"
 
-abbreviation cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60)
+abbreviation cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  (\<open>(If (_)/ then (_)/ else (_))\<close> [0, 0, 60] 60)
   where "If b then e1 else e2 \<equiv> tr_case\<cdot>e1\<cdot>e2\<cdot>b"
 
 translations
   "\<Lambda> (XCONST TT). t" \<rightleftharpoons> "CONST tr_case\<cdot>t\<cdot>\<bottom>"
   "\<Lambda> (XCONST FF). t" \<rightleftharpoons> "CONST tr_case\<cdot>\<bottom>\<cdot>t"

 subsection \<open>Boolean connectives\<close>
 
 definition trand :: "tr \<rightarrow> tr \<rightarrow> tr"
   where andalso_def: "trand = (\<Lambda> x y. If x then y else FF)"
 
-abbreviation andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ andalso _" [36,35] 35)
+abbreviation andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  (\<open>_ andalso _\<close> [36,35] 35)
   where "x andalso y \<equiv> trand\<cdot>x\<cdot>y"
 
 definition tror :: "tr \<rightarrow> tr \<rightarrow> tr"
   where orelse_def: "tror = (\<Lambda> x y. If x then TT else y)"
 
-abbreviation orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ orelse _"  [31,30] 30)
+abbreviation orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  (\<open>_ orelse _\<close>  [31,30] 30)
   where "x orelse y \<equiv> tror\<cdot>x\<cdot>y"
 
 definition neg :: "tr \<rightarrow> tr"
   where "neg = flift2 Not"