equal
deleted
inserted
replaced
42 (type) "mdecl" \<leftharpoondown> (type) "mname \<times> ty \<times> ty \<times> stmt" |
42 (type) "mdecl" \<leftharpoondown> (type) "mname \<times> ty \<times> ty \<times> stmt" |
43 (type) "class" \<leftharpoondown> (type) "cname \<times> fdecl list \<times> mdecl list" |
43 (type) "class" \<leftharpoondown> (type) "cname \<times> fdecl list \<times> mdecl list" |
44 (type) "cdecl" \<leftharpoondown> (type) "cname \<times> class" |
44 (type) "cdecl" \<leftharpoondown> (type) "cname \<times> class" |
45 (type) "prog " \<leftharpoondown> (type) "cdecl list" |
45 (type) "prog " \<leftharpoondown> (type) "cdecl list" |
46 |
46 |
47 consts |
47 axiomatization |
48 |
|
49 Prog :: prog --{* program as a global value *} |
48 Prog :: prog --{* program as a global value *} |
|
49 and |
50 Object :: cname --{* name of root class *} |
50 Object :: cname --{* name of root class *} |
51 |
51 |
52 |
52 |
53 definition "class" :: "cname \<rightharpoonup> class" where |
53 definition "class" :: "cname \<rightharpoonup> class" where |
54 "class \<equiv> map_of Prog" |
54 "class \<equiv> map_of Prog" |