src/HOL/Bali/Example.thy
changeset 30235 58d147683393
parent 28524 644b62cf678f
child 31166 a90fe83f58ea
equal deleted inserted replaced
30224:79136ce06bdb 30235:58d147683393
   456 
   456 
   457 lemmas imethds_rec' = imethds_rec [OF _ ws_tprg]
   457 lemmas imethds_rec' = imethds_rec [OF _ ws_tprg]
   458 lemmas methd_rec'  = methd_rec  [OF _ ws_tprg]
   458 lemmas methd_rec'  = methd_rec  [OF _ ws_tprg]
   459 
   459 
   460 lemma imethds_HasFoo [simp]: 
   460 lemma imethds_HasFoo [simp]: 
   461   "imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
   461   "imethds tprg HasFoo = Option.set \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
   462 apply (rule trans)
   462 apply (rule trans)
   463 apply (rule imethds_rec')
   463 apply (rule imethds_rec')
   464 apply  (auto simp add: HasFooInt_def)
   464 apply  (auto simp add: HasFooInt_def)
   465 done
   465 done
   466 
   466