src/HOL/TLA/Stfun.thy
changeset 80914 d97fdabd9e2b
parent 62145 5b946c81dfbf
--- a/src/HOL/TLA/Stfun.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/TLA/Stfun.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -33,8 +33,8 @@
   stvars    :: "'a stfun \<Rightarrow> bool"
 
 syntax
-  "_PRED"   :: "lift \<Rightarrow> 'a"                          ("PRED _")
-  "_stvars" :: "lift \<Rightarrow> bool"                        ("basevars _")
+  "_PRED"   :: "lift \<Rightarrow> 'a"                          (\<open>PRED _\<close>)
+  "_stvars" :: "lift \<Rightarrow> bool"                        (\<open>basevars _\<close>)
 
 translations
   "PRED P"   =>  "(P::state \<Rightarrow> _)"