equal
deleted
inserted
replaced
326 ==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)" |
326 ==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)" |
327 apply(rule conforms_hext) |
327 apply(rule conforms_hext) |
328 apply auto |
328 apply auto |
329 apply(rule hconfI) |
329 apply(rule hconfI) |
330 apply(drule conforms_heapD) |
330 apply(drule conforms_heapD) |
331 apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] |
331 apply(tactic {* auto_tac (HOL_cs addEs [@{thm oconf_hext}] |
332 addDs [thm "hconfD"], @{simpset} delsimps [split_paired_All]) *}) |
332 addDs [@{thm hconfD}], @{simpset} delsimps [@{thm split_paired_All}]) *}) |
333 done |
333 done |
334 |
334 |
335 lemma conforms_upd_local: |
335 lemma conforms_upd_local: |
336 "[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] |
336 "[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] |
337 ==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)" |
337 ==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)" |