1.1 --- a/src/HOL/Bali/Example.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4  lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn"
     1.5  by (simp add: SXcpt_def)
     1.6  
     1.7 -lemma neq_Main_Object [simp]: "Main\<noteq>SXcpt xn"
     1.8 +lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
     1.9  by (simp add: SXcpt_def)
    1.10  
    1.11  section "classes and interfaces"
    1.12 @@ -687,10 +687,6 @@
    1.13    "tprg\<turnstile>(Base,mdecl Base_foo) member_in Base"
    1.14  by (rule member_of_to_member_in [OF Base_foo_member_of_Base])
    1.15  
    1.16 -lemma Base_foo_member_of_Base: 
    1.17 -  "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
    1.18 -by (auto intro!: members.Immediate Base_declares_foo)
    1.19 -
    1.20  lemma Ext_foo_member_of_Ext: 
    1.21    "tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
    1.22  by (auto intro!: members.Immediate Ext_declares_foo)