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/IMP/Compiler2.thy
changeset 80914 d97fdabd9e2b
parent 80612 e65eed943bee 
--- a/src/HOL/IMP/Compiler2.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/IMP/Compiler2.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -16,7 +16,7 @@
 text \<open>Execution in \<^term>\<open>n\<close> steps for simpler induction\<close>
 primrec 
   exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool" 
-  ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,1000,55] 55)
+  (\<open>_/ \<turnstile> (_ \<rightarrow>^_/ _)\<close> [65,0,1000,55] 55)
 where 
   "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" |
   "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')"
isabelle