1.1 --- a/src/HOL/Bali/WellType.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/HOL/Bali/WellType.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -518,14 +518,15 @@
     1.4  lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
     1.5  by (auto simp add: is_acc_iface_def)
     1.6  
     1.7 -lemma is_acc_iface_is_accessible: 
     1.8 +lemma is_acc_iface_Iface_is_accessible: 
     1.9    "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
    1.10  by (auto simp add: is_acc_iface_def)
    1.11  
    1.12  lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
    1.13  by (auto simp add: is_acc_type_def)
    1.14  
    1.15 -lemma is_acc_iface_is_accessible: "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
    1.16 +lemma is_acc_iface_is_accessible:
    1.17 +  "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
    1.18  by (auto simp add: is_acc_type_def)
    1.19  
    1.20  lemma wt_Methd_is_methd: 
    1.21 @@ -539,13 +540,6 @@
    1.22   * conclusion (no selectors in the conclusion\<dots>)
    1.23   *)
    1.24  
    1.25 -lemma wt_Super:
    1.26 -"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
    1.27 -  class (prg E) C = Some c;D=super c\<rbrakk> 
    1.28 - \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
    1.29 -by (auto elim: wt.Super)
    1.30 - 
    1.31 -
    1.32  lemma wt_Call: 
    1.33  "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
    1.34    max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr>