equal
deleted
inserted
replaced
24 |
24 |
25 text{* Method declaration *} |
25 text{* Method declaration *} |
26 types mdecl |
26 types mdecl |
27 = "mname \<times> methd" |
27 = "mname \<times> methd" |
28 |
28 |
29 record class |
29 record "class" |
30 = super :: cname |
30 = super :: cname |
31 flds ::"fdecl list" |
31 flds ::"fdecl list" |
32 methods ::"mdecl list" |
32 methods ::"mdecl list" |
33 |
33 |
34 text{* Class declaration *} |
34 text{* Class declaration *} |
50 Prog :: prog --{* program as a global value *} |
50 Prog :: prog --{* program as a global value *} |
51 Object :: cname --{* name of root class *} |
51 Object :: cname --{* name of root class *} |
52 |
52 |
53 |
53 |
54 constdefs |
54 constdefs |
55 class :: "cname \<rightharpoonup> class" |
55 "class" :: "cname \<rightharpoonup> class" |
56 "class \<equiv> map_of Prog" |
56 "class \<equiv> map_of Prog" |
57 |
57 |
58 is_class :: "cname => bool" |
58 is_class :: "cname => bool" |
59 "is_class C \<equiv> class C \<noteq> None" |
59 "is_class C \<equiv> class C \<noteq> None" |
60 |
60 |