src/HOL/Bali/Type.thy
changeset 32960 69916a850301
parent 16417 9bc16273c2d4
child 35067 af4c18c30593
     1.1 --- a/src/HOL/Bali/Type.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Bali/Type.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -15,21 +15,21 @@
     1.4  \end{itemize}
     1.5  *}
     1.6  
     1.7 -datatype prim_ty       	--{* primitive type, cf. 4.2 *}
     1.8 -	= Void    	--{* result type of void methods *}
     1.9 -	| Boolean
    1.10 -	| Integer
    1.11 +datatype prim_ty        --{* primitive type, cf. 4.2 *}
    1.12 +        = Void          --{* result type of void methods *}
    1.13 +        | Boolean
    1.14 +        | Integer
    1.15  
    1.16  
    1.17 -datatype ref_ty		--{* reference type, cf. 4.3 *}
    1.18 -	= NullT		--{* null type, cf. 4.1 *}
    1.19 -	| IfaceT qtname	--{* interface type *}
    1.20 -	| ClassT qtname	--{* class type *}
    1.21 -	| ArrayT ty	--{* array type *}
    1.22 +datatype ref_ty         --{* reference type, cf. 4.3 *}
    1.23 +        = NullT         --{* null type, cf. 4.1 *}
    1.24 +        | IfaceT qtname --{* interface type *}
    1.25 +        | ClassT qtname --{* class type *}
    1.26 +        | ArrayT ty     --{* array type *}
    1.27  
    1.28 -and ty	    		--{* any type, cf. 4.1 *}
    1.29 -	= PrimT prim_ty	--{* primitive type *}
    1.30 -	| RefT  ref_ty	--{* reference type *}
    1.31 +and ty                  --{* any type, cf. 4.1 *}
    1.32 +        = PrimT prim_ty --{* primitive type *}
    1.33 +        | RefT  ref_ty  --{* reference type *}
    1.34  
    1.35  translations
    1.36    "prim_ty" <= (type) "Type.prim_ty"
    1.37 @@ -37,16 +37,16 @@
    1.38    "ty"      <= (type) "Type.ty"
    1.39  
    1.40  syntax
    1.41 -	 NT	:: "       \<spacespace> ty"
    1.42 -	 Iface	:: "qtname  \<Rightarrow> ty"
    1.43 -	 Class	:: "qtname  \<Rightarrow> ty"
    1.44 -	 Array	:: "ty     \<Rightarrow> ty"	("_.[]" [90] 90)
    1.45 +         NT     :: "       \<spacespace> ty"
    1.46 +         Iface  :: "qtname  \<Rightarrow> ty"
    1.47 +         Class  :: "qtname  \<Rightarrow> ty"
    1.48 +         Array  :: "ty     \<Rightarrow> ty"    ("_.[]" [90] 90)
    1.49  
    1.50  translations
    1.51 -	"NT"      == "RefT   NullT"
    1.52 -	"Iface I" == "RefT (IfaceT I)"
    1.53 -	"Class C" == "RefT (ClassT C)"
    1.54 -	"T.[]"    == "RefT (ArrayT T)"
    1.55 +        "NT"      == "RefT   NullT"
    1.56 +        "Iface I" == "RefT (IfaceT I)"
    1.57 +        "Class C" == "RefT (ClassT C)"
    1.58 +        "T.[]"    == "RefT (ArrayT T)"
    1.59  
    1.60  constdefs
    1.61    the_Class :: "ty \<Rightarrow> qtname"