equal
deleted
inserted
replaced
282 map_of (map (\<lambda>(s, f). (s, C, f)) fs)" |
282 map_of (map (\<lambda>(s, f). (s, C, f)) fs)" |
283 apply (simp only: field_def) |
283 apply (simp only: field_def) |
284 apply (frule fields_rec, assumption) |
284 apply (frule fields_rec, assumption) |
285 apply (rule HOL.trans) |
285 apply (rule HOL.trans) |
286 apply (simp add: o_def) |
286 apply (simp add: o_def) |
287 apply (simp (no_asm_use) |
287 apply (simp (no_asm_use) add: split_beta split_def o_def) |
288 add: split_beta split_def o_def map_compose [THEN sym] del: map_compose) |
|
289 done |
288 done |
290 |
289 |
291 lemma method_Object [simp]: |
290 lemma method_Object [simp]: |
292 "method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> ws_prog G \<Longrightarrow> D = Object" |
291 "method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> ws_prog G \<Longrightarrow> D = Object" |
293 apply (frule class_Object, clarify) |
292 apply (frule class_Object, clarify) |