--- a/src/HOL/HOLCF/Tr.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/Tr.thy Fri Sep 20 19:51:08 2024 +0200
@@ -63,7 +63,7 @@
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
@@ -82,13 +82,13 @@
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"