--- a/src/HOL/Bali/WellType.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Bali/WellType.thy Tue Aug 27 11:03:05 2002 +0200
@@ -518,14 +518,15 @@
lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
by (auto simp add: is_acc_iface_def)
-lemma is_acc_iface_is_accessible:
+lemma is_acc_iface_Iface_is_accessible:
"is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
by (auto simp add: is_acc_iface_def)
lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
by (auto simp add: is_acc_type_def)
-lemma is_acc_iface_is_accessible: "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
+lemma is_acc_iface_is_accessible:
+ "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
by (auto simp add: is_acc_type_def)
lemma wt_Methd_is_methd:
@@ -539,13 +540,6 @@
* conclusion (no selectors in the conclusion\<dots>)
*)
-lemma wt_Super:
-"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
- class (prg E) C = Some c;D=super c\<rbrakk>
- \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
-by (auto elim: wt.Super)
-
-
lemma wt_Call:
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr>