equal
deleted
inserted
replaced
560 done |
560 done |
561 |
561 |
562 lemma class_Object [simp]: |
562 lemma class_Object [simp]: |
563 "wf_prog G \<Longrightarrow> |
563 "wf_prog G \<Longrightarrow> |
564 class G Object = Some \<lparr>access=Public,cfields=[],methods=Object_mdecls, |
564 class G Object = Some \<lparr>access=Public,cfields=[],methods=Object_mdecls, |
565 init=Skip,super=arbitrary,superIfs=[]\<rparr>" |
565 init=Skip,super=undefined,superIfs=[]\<rparr>" |
566 apply (unfold wf_prog_def Let_def ObjectC_def) |
566 apply (unfold wf_prog_def Let_def ObjectC_def) |
567 apply (fast dest!: map_of_SomeI) |
567 apply (fast dest!: map_of_SomeI) |
568 done |
568 done |
569 |
569 |
570 lemma methd_Object[simp]: "wf_prog G \<Longrightarrow> methd G Object = |
570 lemma methd_Object[simp]: "wf_prog G \<Longrightarrow> methd G Object = |