src/HOL/MicroJava/J/Type.thy
changeset 35102 cc7a0b9f938c
parent 16417 9bc16273c2d4
child 44035 322d1657c40c
     1.1 --- a/src/HOL/MicroJava/J/Type.thy	Wed Feb 10 23:53:46 2010 +0100
     1.2 +++ b/src/HOL/MicroJava/J/Type.thy	Thu Feb 11 00:45:02 2010 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/MicroJava/J/Type.thy
     1.5 -    ID:         $Id$
     1.6      Author:     David von Oheimb
     1.7      Copyright   1999 Technische Universitaet Muenchen
     1.8  *)
     1.9 @@ -47,12 +46,10 @@
    1.10    = PrimT prim_ty -- "primitive type"
    1.11    | RefT  ref_ty  -- "reference type"
    1.12  
    1.13 -syntax
    1.14 -  NT    :: "ty"
    1.15 -  Class :: "cname  => ty"
    1.16 +abbreviation NT :: ty
    1.17 +  where "NT == RefT NullT"
    1.18  
    1.19 -translations
    1.20 -  "NT"      == "RefT NullT"
    1.21 -  "Class C" == "RefT (ClassT C)"
    1.22 +abbreviation Class :: "cname  => ty"
    1.23 +  where "Class C == RefT (ClassT C)"
    1.24  
    1.25  end