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