1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Thu Nov 25 12:30:57 1999 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Nov 26 08:46:59 1999 +0100
     1.3 @@ -32,8 +32,8 @@
     1.4    
     1.5  consts
     1.6  
     1.7 -  cmethd	:: "'c prog \\<times> cname \\<Rightarrow> ( sig   \\<leadsto> cname \\<times> ty \\<times> 'c)"
     1.8 -  cfield	:: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
     1.9 +  method	:: "'c prog \\<times> cname \\<Rightarrow> ( sig   \\<leadsto> cname \\<times> ty \\<times> 'c)"
    1.10 +  field	:: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
    1.11    fields	:: "'c prog \\<times> cname \\<Rightarrow> ((vname \\<times> cname) \\<times>  ty) list"
    1.12  
    1.13  constdefs       (* auxiliary relations for recursive definitions below *)
    1.14 @@ -42,10 +42,10 @@
    1.15   "subcls1_rel \\<equiv> {((G,C),(G',C')). G = G' \\<and>  wf ((subcls1 G)^-1) \\<and>  G\\<turnstile>C'\\<prec>C1C}"
    1.16  
    1.17  (* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
    1.18 -recdef cmethd "subcls1_rel"
    1.19 - "cmethd (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty
    1.20 +recdef method "subcls1_rel"
    1.21 + "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty
    1.22                     | Some (sc,fs,ms) \\<Rightarrow> (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> 
    1.23 -                                           if is_class G D then cmethd (G,D) 
    1.24 +                                           if is_class G D then method (G,D) 
    1.25                                                             else arbitrary) \\<oplus>
    1.26                                             map_of (map (\\<lambda>(s,  m ). 
    1.27                                                          (s,(C,m))) ms))
    1.28 @@ -61,7 +61,7 @@
    1.29                    else arbitrary)"
    1.30  defs
    1.31  
    1.32 -  cfield_def "cfield \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
    1.33 +  field_def "field \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
    1.34  
    1.35  inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
    1.36  			     i.e. sort of syntactic subtyping *)