src/HOL/MicroJava/J/Conform.thy
changeset 42793 88bee9f6eec7
parent 42463 f270e3e18be5
child 42795 66fcc9882784
equal deleted inserted replaced
42792:85fb70b0c5e8 42793:88bee9f6eec7
   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 {*
   332                 addDs [@{thm hconfD}], @{simpset} delsimps [@{thm split_paired_All}]) *})
   332   auto_tac (put_claset HOL_cs @{context} addEs [@{thm oconf_hext}] addDs [@{thm hconfD}]
       
   333   |> map_simpset_local (fn ss => ss delsimps [@{thm split_paired_All}])) *})
   333 done
   334 done
   334 
   335 
   335 lemma conforms_upd_local: 
   336 lemma conforms_upd_local: 
   336 "[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] 
   337 "[|(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)"
   338   ==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)"