src/HOL/MicroJava/BV/Correct.thy
changeset 13681 06cce9be31a4
parent 13052 3bf41c474a88
child 16417 9bc16273c2d4
equal deleted inserted replaced
13680:a6ce43a59d4a 13681:06cce9be31a4
   332 
   332 
   333 lemma correct_frames_newref [rule_format]:
   333 lemma correct_frames_newref [rule_format]:
   334   "\<forall>rT C sig. 
   334   "\<forall>rT C sig. 
   335   hp x = None \<longrightarrow> 
   335   hp x = None \<longrightarrow> 
   336   correct_frames G hp phi rT sig frs \<longrightarrow>
   336   correct_frames G hp phi rT sig frs \<longrightarrow>
   337   G,hp \<turnstile> obj \<surd>
   337   correct_frames G (hp(x \<mapsto> obj)) phi rT sig frs"
   338   \<longrightarrow> correct_frames G (hp(x \<mapsto> obj)) phi rT sig frs"
       
   339 apply (induct frs)
   338 apply (induct frs)
   340  apply simp
   339  apply simp
   341 apply clarify
   340 apply clarify
   342 apply (simp (no_asm_use))
   341 apply (simp (no_asm_use))
   343 apply clarify
   342 apply clarify