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/Bali/Trans.thy
changeset 80914 d97fdabd9e2b
parent 67443 3abf6a722518 
--- a/src/HOL/Bali/Trans.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Bali/Trans.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -56,7 +56,7 @@
   where "SKIP == Lit Unit"
 
 inductive
-  step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
+  step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" (\<open>_\<turnstile>_ \<mapsto>1 _\<close>[61,82,82] 81)
   for G :: prog
 where
 
@@ -344,11 +344,11 @@
     "G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
 
 abbreviation
-  stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
+  stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" (\<open>_\<turnstile>_ \<mapsto>_ _\<close>[61,82,82] 81)
   where "G\<turnstile>p \<mapsto>n p' \<equiv> (p,p') \<in> {(x, y). step G x y}^^n"
 
 abbreviation
-  steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
+  steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" (\<open>_\<turnstile>_ \<mapsto>* _\<close>[61,82,82] 81)
   where "G\<turnstile>p \<mapsto>* p' \<equiv> (p,p') \<in> {(x, y). step G x y}\<^sup>*"
          
 (* Equivalenzen:
isabelle