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> _)"