src/HOL/NanoJava/Term.thy
changeset 11499 7a7bb59a05db
parent 11497 0e66e0114d9a
child 11507 4b32a46ffd29
equal deleted inserted replaced
11498:681aa3dfab4b 11499:7a7bb59a05db
     9 theory Term = Main:
     9 theory Term = Main:
    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 types   imname = "cname \<times> mname"
    14 types   imname = "cname \<times> mname"
    18 
    15 
    19 datatype vname  (* variable for special names *)
    16 datatype vname  (* variable for special names *)
    20   = This        (* This pointer *)
    17   = This        (* This pointer *)
    21   | Param       (* method parameter *)
    18   | Param       (* method parameter *)