src/HOL/MicroJava/J/Type.thy
changeset 12951 a9fdcb71d252
parent 12911 704713ca07ea
child 16417 9bc16273c2d4
equal deleted inserted replaced
12950:3aadb133632d 12951:a9fdcb71d252
    19 
    19 
    20 -- "class names"
    20 -- "class names"
    21 datatype cname  
    21 datatype cname  
    22   = Object 
    22   = Object 
    23   | Xcpt xcpt 
    23   | Xcpt xcpt 
    24   | Cname cname 
    24   | Cname cnam 
    25 
    25 
    26 typedecl vnam   -- "variable or field name"
    26 typedecl vnam   -- "variable or field name"
    27 typedecl mname  -- "method name"
    27 typedecl mname  -- "method name"
    28 
    28 
    29 -- "names for @{text This} pointer and local/field variables"
    29 -- "names for @{text This} pointer and local/field variables"