diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/TLA/Intensional.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -33,11 +33,11 @@
   where unl_lift3: "lift3 f x y z w \<equiv> f (x w) (y w) (z w)"
 
 (* "Rigid" quantification (logic level) *)
-definition RAll :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"  (binder "Rall " 10)
+definition RAll :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"  (binder \<open>Rall \<close> 10)
   where unl_Rall: "(Rall x. A x) w \<equiv> \<forall>x. A x w"
-definition REx :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"  (binder "Rex " 10)
+definition REx :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"  (binder \<open>Rex \<close> 10)
   where unl_Rex: "(Rex x. A x) w \<equiv> \<exists>x. A x w"
-definition REx1 :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"  (binder "Rex! " 10)
+definition REx1 :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"  (binder \<open>Rex! \<close> 10)
   where unl_Rex1: "(Rex! x. A x) w \<equiv> \<exists>!x. A x w"
 
 
@@ -46,56 +46,56 @@
 nonterminal lift and liftargs
 
 syntax
-  ""            :: "id \<Rightarrow> lift"                          ("_")
-  ""            :: "longid \<Rightarrow> lift"                      ("_")
-  ""            :: "var \<Rightarrow> lift"                         ("_")
-  "_applC"      :: "[lift, cargs] \<Rightarrow> lift"               ("(1_/ _)" [1000, 1000] 999)
-  ""            :: "lift \<Rightarrow> lift"                        ("'(_')")
-  "_lambda"     :: "[idts, 'a] \<Rightarrow> lift"                  ("(3\<lambda>_./ _)" [0, 3] 3)
-  "_constrain"  :: "[lift, type] \<Rightarrow> lift"                ("(_::_)" [4, 0] 3)
-  ""            :: "lift \<Rightarrow> liftargs"                    ("_")
-  "_liftargs"   :: "[lift, liftargs] \<Rightarrow> liftargs"        ("_,/ _")
-  "_Valid"      :: "lift \<Rightarrow> bool"                        ("(\<turnstile> _)" 5)
-  "_holdsAt"    :: "['a, lift] \<Rightarrow> bool"                  ("(_ \<Turnstile> _)" [100,10] 10)
+  ""            :: "id \<Rightarrow> lift"                          (\<open>_\<close>)
+  ""            :: "longid \<Rightarrow> lift"                      (\<open>_\<close>)
+  ""            :: "var \<Rightarrow> lift"                         (\<open>_\<close>)
+  "_applC"      :: "[lift, cargs] \<Rightarrow> lift"               (\<open>(1_/ _)\<close> [1000, 1000] 999)
+  ""            :: "lift \<Rightarrow> lift"                        (\<open>'(_')\<close>)
+  "_lambda"     :: "[idts, 'a] \<Rightarrow> lift"                  (\<open>(3\<lambda>_./ _)\<close> [0, 3] 3)
+  "_constrain"  :: "[lift, type] \<Rightarrow> lift"                (\<open>(_::_)\<close> [4, 0] 3)
+  ""            :: "lift \<Rightarrow> liftargs"                    (\<open>_\<close>)
+  "_liftargs"   :: "[lift, liftargs] \<Rightarrow> liftargs"        (\<open>_,/ _\<close>)
+  "_Valid"      :: "lift \<Rightarrow> bool"                        (\<open>(\<turnstile> _)\<close> 5)
+  "_holdsAt"    :: "['a, lift] \<Rightarrow> bool"                  (\<open>(_ \<Turnstile> _)\<close> [100,10] 10)
 
   (* Syntax for lifted expressions outside the scope of \<turnstile> or |= *)
-  "_LIFT"       :: "lift \<Rightarrow> 'a"                          ("LIFT _")
+  "_LIFT"       :: "lift \<Rightarrow> 'a"                          (\<open>LIFT _\<close>)
 
   (* generic syntax for lifted constants and functions *)
-  "_const"      :: "'a \<Rightarrow> lift"                          ("(#_)" [1000] 999)
-  "_lift"       :: "['a, lift] \<Rightarrow> lift"                  ("(_<_>)" [1000] 999)
-  "_lift2"      :: "['a, lift, lift] \<Rightarrow> lift"            ("(_<_,/ _>)" [1000] 999)
-  "_lift3"      :: "['a, lift, lift, lift] \<Rightarrow> lift"      ("(_<_,/ _,/ _>)" [1000] 999)
+  "_const"      :: "'a \<Rightarrow> lift"                          (\<open>(#_)\<close> [1000] 999)
+  "_lift"       :: "['a, lift] \<Rightarrow> lift"                  (\<open>(_<_>)\<close> [1000] 999)
+  "_lift2"      :: "['a, lift, lift] \<Rightarrow> lift"            (\<open>(_<_,/ _>)\<close> [1000] 999)
+  "_lift3"      :: "['a, lift, lift, lift] \<Rightarrow> lift"      (\<open>(_<_,/ _,/ _>)\<close> [1000] 999)
 
   (* concrete syntax for common infix functions: reuse same symbol *)
-  "_liftEqu"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ =/ _)" [50,51] 50)
-  "_liftNeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ \<noteq>/ _)" [50,51] 50)
-  "_liftNot"    :: "lift \<Rightarrow> lift"                        ("(\<not> _)" [40] 40)
-  "_liftAnd"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ \<and>/ _)" [36,35] 35)
-  "_liftOr"     :: "[lift, lift] \<Rightarrow> lift"                ("(_ \<or>/ _)" [31,30] 30)
-  "_liftImp"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ \<longrightarrow>/ _)" [26,25] 25)
-  "_liftIf"     :: "[lift, lift, lift] \<Rightarrow> lift"          ("(if (_)/ then (_)/ else (_))" 10)
-  "_liftPlus"   :: "[lift, lift] \<Rightarrow> lift"                ("(_ +/ _)" [66,65] 65)
-  "_liftMinus"  :: "[lift, lift] \<Rightarrow> lift"                ("(_ -/ _)" [66,65] 65)
-  "_liftTimes"  :: "[lift, lift] \<Rightarrow> lift"                ("(_ */ _)" [71,70] 70)
-  "_liftDiv"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ div _)" [71,70] 70)
-  "_liftMod"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ mod _)" [71,70] 70)
-  "_liftLess"   :: "[lift, lift] \<Rightarrow> lift"                ("(_/ < _)"  [50, 51] 50)
-  "_liftLeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<le> _)" [50, 51] 50)
-  "_liftMem"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<in> _)" [50, 51] 50)
-  "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<notin> _)" [50, 51] 50)
-  "_liftFinset" :: "liftargs \<Rightarrow> lift"                    ("{(_)}")
+  "_liftEqu"    :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_ =/ _)\<close> [50,51] 50)
+  "_liftNeq"    :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_ \<noteq>/ _)\<close> [50,51] 50)
+  "_liftNot"    :: "lift \<Rightarrow> lift"                        (\<open>(\<not> _)\<close> [40] 40)
+  "_liftAnd"    :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_ \<and>/ _)\<close> [36,35] 35)
+  "_liftOr"     :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_ \<or>/ _)\<close> [31,30] 30)
+  "_liftImp"    :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_ \<longrightarrow>/ _)\<close> [26,25] 25)
+  "_liftIf"     :: "[lift, lift, lift] \<Rightarrow> lift"          (\<open>(if (_)/ then (_)/ else (_))\<close> 10)
+  "_liftPlus"   :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_ +/ _)\<close> [66,65] 65)
+  "_liftMinus"  :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_ -/ _)\<close> [66,65] 65)
+  "_liftTimes"  :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_ */ _)\<close> [71,70] 70)
+  "_liftDiv"    :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_ div _)\<close> [71,70] 70)
+  "_liftMod"    :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_ mod _)\<close> [71,70] 70)
+  "_liftLess"   :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_/ < _)\<close>  [50, 51] 50)
+  "_liftLeq"    :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_/ \<le> _)\<close> [50, 51] 50)
+  "_liftMem"    :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_/ \<in> _)\<close> [50, 51] 50)
+  "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift"                (\<open>(_/ \<notin> _)\<close> [50, 51] 50)
+  "_liftFinset" :: "liftargs \<Rightarrow> lift"                    (\<open>{(_)}\<close>)
   (** TODO: syntax for lifted collection / comprehension **)
-  "_liftPair"   :: "[lift,liftargs] \<Rightarrow> lift"                   ("(1'(_,/ _'))")
+  "_liftPair"   :: "[lift,liftargs] \<Rightarrow> lift"                   (\<open>(1'(_,/ _'))\<close>)
   (* infix syntax for list operations *)
-  "_liftCons" :: "[lift, lift] \<Rightarrow> lift"                  ("(_ #/ _)" [65,66] 65)
-  "_liftApp"  :: "[lift, lift] \<Rightarrow> lift"                  ("(_ @/ _)" [65,66] 65)
-  "_liftList" :: "liftargs \<Rightarrow> lift"                      ("[(_)]")
+  "_liftCons" :: "[lift, lift] \<Rightarrow> lift"                  (\<open>(_ #/ _)\<close> [65,66] 65)
+  "_liftApp"  :: "[lift, lift] \<Rightarrow> lift"                  (\<open>(_ @/ _)\<close> [65,66] 65)
+  "_liftList" :: "liftargs \<Rightarrow> lift"                      (\<open>[(_)]\<close>)
 
   (* Rigid quantification (syntax level) *)
-  "_RAll" :: "[idts, lift] \<Rightarrow> lift"                      ("(3\<forall>_./ _)" [0, 10] 10)
-  "_REx"  :: "[idts, lift] \<Rightarrow> lift"                      ("(3\<exists>_./ _)" [0, 10] 10)
-  "_REx1" :: "[idts, lift] \<Rightarrow> lift"                      ("(3\<exists>!_./ _)" [0, 10] 10)
+  "_RAll" :: "[idts, lift] \<Rightarrow> lift"                      (\<open>(3\<forall>_./ _)\<close> [0, 10] 10)
+  "_REx"  :: "[idts, lift] \<Rightarrow> lift"                      (\<open>(3\<exists>_./ _)\<close> [0, 10] 10)
+  "_REx1" :: "[idts, lift] \<Rightarrow> lift"                      (\<open>(3\<exists>!_./ _)\<close> [0, 10] 10)
 
 translations
   "_const"        == "CONST const"