--- a/src/HOL/IMP/Compiler0.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/IMP/Compiler0.thy Mon Apr 20 09:32:07 2009 +0200
@@ -45,7 +45,7 @@
abbreviation
stepan :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50) where
- "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : ((stepa1 P)^i)"
+ "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : (stepa1 P ^^ i)"
subsection "The compiler"