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 {* |
331 apply(auto elim: oconf_hext dest: hconfD) |
332 auto_tac (put_claset HOL_cs @{context} addEs [@{thm oconf_hext}] addDs [@{thm hconfD}] |
|
333 |> map_simpset (fn ss => ss delsimps [@{thm split_paired_All}])) *}) |
|
334 done |
332 done |
335 |
333 |
336 lemma conforms_upd_local: |
334 lemma conforms_upd_local: |
337 "[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] |
335 "[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] |
338 ==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)" |
336 ==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)" |