src/HOL/MicroJava/J/Type.thy
changeset 12338 de0f4a63baa5
parent 11070 cc421547e744
child 12517 360e3215f029
equal deleted inserted replaced
12337:7c6a970f0808 12338:de0f4a63baa5
     9 theory Type = JBasis:
     9 theory Type = JBasis:
    10 
    10 
    11 typedecl cname  (* class name *)
    11 typedecl cname  (* class name *)
    12 typedecl vnam   (* variable or field name *)
    12 typedecl vnam   (* variable or field name *)
    13 typedecl mname  (* method name *)
    13 typedecl mname  (* method name *)
    14 arities  cname :: "term"
       
    15          vnam  :: "term"
       
    16          mname :: "term"
       
    17 
    14 
    18 datatype vname    (* names for This pointer and local/field variables *)
    15 datatype vname    (* names for This pointer and local/field variables *)
    19   = This
    16   = This
    20   | VName vnam
    17   | VName vnam
    21 
    18