--- a/src/HOL/IMP/Compiler.thy Tue Dec 18 21:28:01 2001 +0100
+++ b/src/HOL/IMP/Compiler.thy Wed Dec 19 00:26:04 2001 +0100
@@ -19,15 +19,15 @@
consts stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
syntax
- "@stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+ "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)
- "@stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+ "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)
syntax (xsymbols)
- "@stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+ "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
("_ \<turnstile> \<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
- "@stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+ "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
("_ \<turnstile>/ \<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
translations