src/HOL/MicroJava/Comp/CorrCompTp.thy
changeset 33954 1bc3b688548c
parent 33640 0d82107dc07a
child 35102 cc7a0b9f938c
     1.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Dec 02 12:04:07 2009 +0100
     1.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Nov 24 14:37:23 2009 +0100
     1.3 @@ -1122,6 +1122,8 @@
     1.4  apply simp+
     1.5  done
     1.6  
     1.7 +declare not_Err_eq [iff del]
     1.8 +
     1.9  lemma bc_mt_corresp_Load: "\<lbrakk> i < length LT; LT ! i \<noteq> Err; mxr = length LT \<rbrakk>
    1.10    \<Longrightarrow> bc_mt_corresp [Load i] 
    1.11           (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
    1.12 @@ -1138,7 +1140,7 @@
    1.13    apply (frule listE_nth_in) apply assumption
    1.14  apply (subgoal_tac "LT ! i \<in> {x. \<exists>y\<in>types cG. x = OK y}")
    1.15  apply (drule CollectD) apply (erule bexE)
    1.16 -apply (simp (no_asm_simp) )
    1.17 +apply (simp (no_asm_simp))
    1.18  apply blast
    1.19  apply blast
    1.20  done