src/HOL/Bali/Type.thy
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 58887 38db8ddc0f57
     1.1 --- a/src/HOL/Bali/Type.thy	Thu Sep 11 19:26:59 2014 +0200
     1.2 +++ b/src/HOL/Bali/Type.thy	Thu Sep 11 19:32:36 2014 +0200
     1.3 @@ -14,13 +14,13 @@
     1.4  \end{itemize}
     1.5  *}
     1.6  
     1.7 -datatype_new prim_ty        --{* primitive type, cf. 4.2 *}
     1.8 +datatype prim_ty        --{* primitive type, cf. 4.2 *}
     1.9          = Void          --{* result type of void methods *}
    1.10          | Boolean
    1.11          | Integer
    1.12  
    1.13  
    1.14 -datatype_new ref_ty         --{* reference type, cf. 4.3 *}
    1.15 +datatype ref_ty         --{* reference type, cf. 4.3 *}
    1.16          = NullT         --{* null type, cf. 4.1 *}
    1.17          | IfaceT qtname --{* interface type *}
    1.18          | ClassT qtname --{* class type *}