equal
deleted
inserted
replaced
544 case True |
544 case True |
545 with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases) |
545 with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases) |
546 then show ?thesis by blast |
546 then show ?thesis by blast |
547 next |
547 next |
548 case False then show ?thesis |
548 case False then show ?thesis |
549 by (auto simp add: invmode_def split: split_if_asm) |
549 by (auto simp add: invmode_def) |
550 qed |
550 qed |
551 qed |
551 qed |
552 |
552 |
553 lemma wt_Super: |
553 lemma wt_Super: |
554 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> |
554 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> |