Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TLA/Memory/ProcedureInterface.thy
changeset 80914 d97fdabd9e2b
parent 66453 cc19f7ca2ed6 
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -41,7 +41,7 @@
   where "slice x i s \<equiv> x s i"
 
 syntax
-  "_slice" :: "[lift, 'a] \<Rightarrow> lift"  ("(_!_)" [70,70] 70)
+  "_slice" :: "[lift, 'a] \<Rightarrow> lift"  (\<open>(_!_)\<close> [70,70] 70)
 translations
   "_slice" \<rightleftharpoons> "CONST slice"
 
@@ -67,8 +67,8 @@
     \<and> (res<ch!p>$ = $v)"
 
 syntax
-  "_Call" :: "['a, 'b, lift] \<Rightarrow> lift"  ("(Call _ _ _)" [90,90,90] 90)
-  "_Return" :: "['a, 'b, lift] \<Rightarrow> lift"  ("(Return _ _ _)" [90,90,90] 90)
+  "_Call" :: "['a, 'b, lift] \<Rightarrow> lift"  (\<open>(Call _ _ _)\<close> [90,90,90] 90)
+  "_Return" :: "['a, 'b, lift] \<Rightarrow> lift"  (\<open>(Return _ _ _)\<close> [90,90,90] 90)
 translations
   "_Call" \<rightleftharpoons> "CONST ACall"
   "_Return" \<rightleftharpoons> "CONST AReturn"
isabelle