src/HOL/Bali/DeclConcepts.thy
changeset 32134 ee143615019c
parent 30235 58d147683393
child 32754 4e0256f7d219
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Wed Jul 22 14:20:31 2009 +0200
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed Jul 22 14:20:32 2009 +0200
     1.3 @@ -648,7 +648,7 @@
     1.4             G \<turnstile>Method old member_of superNew
     1.5             \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
     1.6  
     1.7 -| Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S inter; G\<turnstile>inter overrides\<^sub>S old\<rbrakk>
     1.8 +| Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S intr; G\<turnstile>intr overrides\<^sub>S old\<rbrakk>
     1.9               \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
    1.10  
    1.11  text {* Dynamic overriding (used during the typecheck of the compiler) *}
    1.12 @@ -668,7 +668,7 @@
    1.13             G\<turnstile>resTy new \<preceq> resTy old
    1.14             \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides old"
    1.15  
    1.16 -| Indirect: "\<lbrakk>G\<turnstile>new overrides inter; G\<turnstile>inter overrides old\<rbrakk>
    1.17 +| Indirect: "\<lbrakk>G\<turnstile>new overrides intr; G\<turnstile>intr overrides old\<rbrakk>
    1.18              \<Longrightarrow> G\<turnstile>new overrides old"
    1.19  
    1.20  syntax