equal
deleted
inserted
replaced
28 |
28 |
29 and ty --{* any type, cf. 4.1 *} |
29 and ty --{* any type, cf. 4.1 *} |
30 = PrimT prim_ty --{* primitive type *} |
30 = PrimT prim_ty --{* primitive type *} |
31 | RefT ref_ty --{* reference type *} |
31 | RefT ref_ty --{* reference type *} |
32 |
32 |
33 translations |
|
34 "prim_ty" <= (type) "Type.prim_ty" |
|
35 "ref_ty" <= (type) "Type.ref_ty" |
|
36 "ty" <= (type) "Type.ty" |
|
37 |
|
38 abbreviation "NT == RefT NullT" |
33 abbreviation "NT == RefT NullT" |
39 abbreviation "Iface I == RefT (IfaceT I)" |
34 abbreviation "Iface I == RefT (IfaceT I)" |
40 abbreviation "Class C == RefT (ClassT C)" |
35 abbreviation "Class C == RefT (ClassT C)" |
41 abbreviation Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90) |
36 abbreviation Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90) |
42 where "T.[] == RefT (ArrayT T)" |
37 where "T.[] == RefT (ArrayT T)" |