equal
deleted
inserted
replaced
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 |