src/HOL/MicroJava/J/Type.thy
changeset 8032 1eaae1a2f8ff
parent 8011 d14c4e9e9c8e
child 10042 7164dc0d24d8
     1.1 --- a/src/HOL/MicroJava/J/Type.thy	Wed Nov 24 13:36:14 1999 +0100
     1.2 +++ b/src/HOL/MicroJava/J/Type.thy	Thu Nov 25 12:01:28 1999 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4  datatype ref_ty		(* reference type, cf. 4.3 *)
     1.5  	= NullT		(* null type, cf. 4.1 *)
     1.6  	| ClassT cname	(* class type *)
     1.7 -and ty    		(* any type, cf. 4.1 *)
     1.8 +datatype ty    		(* any type, cf. 4.1 *)
     1.9  	= PrimT prim_ty	(* primitive type *)
    1.10  	| RefT  ref_ty	(* reference type *)
    1.11