equal
deleted
inserted
replaced
13 |
13 |
14 sig = "mname \<times> ty list" -- "signature of a method, cf. 8.4.2" |
14 sig = "mname \<times> ty list" -- "signature of a method, cf. 8.4.2" |
15 |
15 |
16 'c mdecl = "sig \<times> ty \<times> 'c" -- "method declaration in a class" |
16 'c mdecl = "sig \<times> ty \<times> 'c" -- "method declaration in a class" |
17 |
17 |
18 'c class = "cname \<times> fdecl list \<times> 'c mdecl list" |
18 'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list" |
19 -- "class = superclass, fields, methods" |
19 -- "class = superclass, fields, methods" |
20 |
20 |
21 'c cdecl = "cname \<times> 'c class" -- "class declaration, cf. 8.1" |
21 'c cdecl = "cname \<times> 'c class" -- "class declaration, cf. 8.1" |
22 |
22 |
23 'c prog = "'c cdecl list" -- "program" |
23 'c prog = "'c cdecl list" -- "program" |
31 "cdecl c" <= (type) "cname \<times> (c class)" |
31 "cdecl c" <= (type) "cname \<times> (c class)" |
32 "prog c" <= (type) "(c cdecl) list" |
32 "prog c" <= (type) "(c cdecl) list" |
33 |
33 |
34 |
34 |
35 constdefs |
35 constdefs |
36 class :: "'c prog => (cname \<rightharpoonup> 'c class)" |
36 "class" :: "'c prog => (cname \<rightharpoonup> 'c class)" |
37 "class \<equiv> map_of" |
37 "class \<equiv> map_of" |
38 |
38 |
39 is_class :: "'c prog => cname => bool" |
39 is_class :: "'c prog => cname => bool" |
40 "is_class G C \<equiv> class G C \<noteq> None" |
40 "is_class G C \<equiv> class G C \<noteq> None" |
41 |
41 |