src/HOL/Bali/Type.thy
changeset 35431 8758fe1fc9f8
parent 35416 d8d7d1b785af
child 37956 ee939247b2fb
     1.1 --- a/src/HOL/Bali/Type.thy	Wed Mar 03 00:32:14 2010 +0100
     1.2 +++ b/src/HOL/Bali/Type.thy	Wed Mar 03 00:33:02 2010 +0100
     1.3 @@ -30,11 +30,6 @@
     1.4          = PrimT prim_ty --{* primitive type *}
     1.5          | RefT  ref_ty  --{* reference type *}
     1.6  
     1.7 -translations
     1.8 -  "prim_ty" <= (type) "Type.prim_ty"
     1.9 -  "ref_ty"  <= (type) "Type.ref_ty"
    1.10 -  "ty"      <= (type) "Type.ty"
    1.11 -
    1.12  abbreviation "NT == RefT NullT"
    1.13  abbreviation "Iface I == RefT (IfaceT I)"
    1.14  abbreviation "Class C == RefT (ClassT C)"