1.1 --- a/src/HOL/IMP/Compiler0.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/IMP/Compiler0.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -39,6 +39,14 @@
     1.4    "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
     1.5                 ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
     1.9 +               ("_ |- (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
    1.10 +  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
    1.11 +               ("_ |-/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
    1.12 +  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
    1.13 +               ("_ |-/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
    1.14 +
    1.15  translations  
    1.16    "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
    1.17    "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"