1.1 --- a/src/HOL/IMP/Comp_Rev.thy	Thu Jul 28 11:49:03 2011 +0200
     1.2 +++ b/src/HOL/IMP/Comp_Rev.thy	Thu Jul 28 15:15:26 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  text {* Execution in @{term n} steps for simpler induction *}
     1.5  primrec 
     1.6    exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool" 
     1.7 -  ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,55,55] 55)
     1.8 +  ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,1000,55] 55)
     1.9  where 
    1.10    "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" |
    1.11    "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')"
    1.12 @@ -41,7 +41,7 @@
    1.13  lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp
    1.14  
    1.15  lemma exec_Suc [trans]:
    1.16 -  "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^Suc n c''" 
    1.17 +  "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''" 
    1.18    by (fastsimp simp del: split_paired_Ex)
    1.19  
    1.20  lemma exec_exec_n: