src/HOL/Bali/DeclConcepts.thy
changeset 22426 1c38ca2496c4
parent 21765 89275a3ed7be
child 23747 b07cff284683
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Fri Mar 09 08:45:57 2007 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Fri Mar 09 08:45:58 2007 +0100
     1.3 @@ -806,8 +806,8 @@
     1.4                  G\<turnstile>(Class class) accessible_in (pid accclass);
     1.5                  membr=(C,mdecl new);
     1.6                  G\<turnstile>(C,new) overrides\<^sub>S old; 
     1.7 -                G\<turnstile>class \<prec>\<^sub>C sup;
     1.8 -                G\<turnstile>Method old of sup accessible_from accclass
     1.9 +                G\<turnstile>class \<prec>\<^sub>C supr;
    1.10 +                G\<turnstile>Method old of supr accessible_from accclass
    1.11                 \<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
    1.12  
    1.13  syntax 
    1.14 @@ -848,8 +848,8 @@
    1.15  | Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
    1.16                  membr=(C,mdecl new);
    1.17                  G\<turnstile>(C,new) overrides old; 
    1.18 -                G\<turnstile>class \<prec>\<^sub>C sup;
    1.19 -                G\<turnstile>Method old in sup dyn_accessible_from accclass
    1.20 +                G\<turnstile>class \<prec>\<^sub>C supr;
    1.21 +                G\<turnstile>Method old in supr dyn_accessible_from accclass
    1.22                 \<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
    1.23  
    1.24  syntax