src/HOL/Bali/DeclConcepts.thy
changeset 14709 d01983034ded
parent 14700 2f885b7e5ba7
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Thu May 06 14:20:13 2004 +0200
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Thu May 06 20:43:30 2004 +0200
     1.3 @@ -163,7 +163,7 @@
     1.4  
     1.5  defs (overloaded)
     1.6  static_field_type_is_static_def: 
     1.7 - "is_static (m::('b::type) member_ext_type) \<equiv> static_val m"
     1.8 + "is_static (m::('b::type) member_ext_type) \<equiv> static_sel m"
     1.9  
    1.10  lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
    1.11  apply (cases m)
    1.12 @@ -412,14 +412,14 @@
    1.13  defs (overloaded)
    1.14  member_ext_type_resTy_def: 
    1.15   "resTy (m::('b::has_resTy) member_ext_type) 
    1.16 -  \<equiv> resTy (member.more_val m)" 
    1.17 +  \<equiv> resTy (member.more_sel m)" 
    1.18  
    1.19  instance mhead_ext_type :: ("type") has_resTy ..
    1.20  
    1.21  defs (overloaded)
    1.22  mhead_ext_type_resTy_def: 
    1.23   "resTy (m::('b mhead_ext_type)) 
    1.24 -  \<equiv> resT_val m" 
    1.25 +  \<equiv> resT_sel m" 
    1.26  
    1.27  lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
    1.28  apply (cases m)