src/HOL/Bali/Example.thy
changeset 13524 604d0f3622d6
parent 12925 99131847fb93
child 13688 a0b16d42d489
--- a/src/HOL/Bali/Example.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Bali/Example.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -126,7 +126,7 @@
 lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn"
 by (simp add: SXcpt_def)
 
-lemma neq_Main_Object [simp]: "Main\<noteq>SXcpt xn"
+lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
 by (simp add: SXcpt_def)
 
 section "classes and interfaces"
@@ -687,10 +687,6 @@
   "tprg\<turnstile>(Base,mdecl Base_foo) member_in Base"
 by (rule member_of_to_member_in [OF Base_foo_member_of_Base])
 
-lemma Base_foo_member_of_Base: 
-  "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
-by (auto intro!: members.Immediate Base_declares_foo)
-
 lemma Ext_foo_member_of_Ext: 
   "tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
 by (auto intro!: members.Immediate Ext_declares_foo)