src/HOL/Bali/Type.thy
changeset 62042 6c6ccf573479
parent 58887 38db8ddc0f57
child 67443 3abf6a722518
     1.1 --- a/src/HOL/Bali/Type.thy	Sat Jan 02 18:46:36 2016 +0100
     1.2 +++ b/src/HOL/Bali/Type.thy	Sat Jan 02 18:48:45 2016 +0100
     1.3 @@ -2,33 +2,33 @@
     1.4      Author:     David von Oheimb
     1.5  *)
     1.6  
     1.7 -subsection {* Java types *}
     1.8 +subsection \<open>Java types\<close>
     1.9  
    1.10  theory Type imports Name begin
    1.11  
    1.12 -text {*
    1.13 +text \<open>
    1.14  simplifications:
    1.15  \begin{itemize}
    1.16  \item only the most important primitive types
    1.17  \item the null type is regarded as reference type
    1.18  \end{itemize}
    1.19 -*}
    1.20 +\<close>
    1.21  
    1.22 -datatype prim_ty        --{* primitive type, cf. 4.2 *}
    1.23 -        = Void          --{* result type of void methods *}
    1.24 +datatype prim_ty        \<comment>\<open>primitive type, cf. 4.2\<close>
    1.25 +        = Void          \<comment>\<open>result type of void methods\<close>
    1.26          | Boolean
    1.27          | Integer
    1.28  
    1.29  
    1.30 -datatype ref_ty         --{* reference type, cf. 4.3 *}
    1.31 -        = NullT         --{* null type, cf. 4.1 *}
    1.32 -        | IfaceT qtname --{* interface type *}
    1.33 -        | ClassT qtname --{* class type *}
    1.34 -        | ArrayT ty     --{* array type *}
    1.35 +datatype ref_ty         \<comment>\<open>reference type, cf. 4.3\<close>
    1.36 +        = NullT         \<comment>\<open>null type, cf. 4.1\<close>
    1.37 +        | IfaceT qtname \<comment>\<open>interface type\<close>
    1.38 +        | ClassT qtname \<comment>\<open>class type\<close>
    1.39 +        | ArrayT ty     \<comment>\<open>array type\<close>
    1.40  
    1.41 -and ty                  --{* any type, cf. 4.1 *}
    1.42 -        = PrimT prim_ty --{* primitive type *}
    1.43 -        | RefT  ref_ty  --{* reference type *}
    1.44 +and ty                  \<comment>\<open>any type, cf. 4.1\<close>
    1.45 +        = PrimT prim_ty \<comment>\<open>primitive type\<close>
    1.46 +        | RefT  ref_ty  \<comment>\<open>reference type\<close>
    1.47  
    1.48  abbreviation "NT == RefT NullT"
    1.49  abbreviation "Iface I == RefT (IfaceT I)"