equal
deleted
inserted
replaced
44 "mdecl c" <= (type) "sig \\<times> ty \\<times> c" |
44 "mdecl c" <= (type) "sig \\<times> ty \\<times> c" |
45 "class c" <= (type) "cname \\<times> fdecl list \\<times> (c mdecl) list" |
45 "class c" <= (type) "cname \\<times> fdecl list \\<times> (c mdecl) list" |
46 "cdecl c" <= (type) "cname \\<times> (c class)" |
46 "cdecl c" <= (type) "cname \\<times> (c class)" |
47 "prog c" <= (type) "(c cdecl) list" |
47 "prog c" <= (type) "(c cdecl) list" |
48 |
48 |
49 consts |
49 constdefs |
50 |
50 |
51 class :: "'c prog => (cname \\<leadsto> 'c class)" |
51 class :: "'c prog => (cname \\<leadsto> 'c class)" |
|
52 "class \\<equiv> map_of" |
52 is_class :: "'c prog => cname => bool" |
53 is_class :: "'c prog => cname => bool" |
53 |
54 "is_class G C \\<equiv> class G C \\<noteq> None" |
54 translations |
|
55 |
|
56 "class" => "map_of" |
|
57 "is_class G C" == "class G C \\<noteq> None" |
|
58 |
55 |
59 consts |
56 consts |
60 |
57 |
61 is_type :: "'c prog => ty => bool" |
58 is_type :: "'c prog => ty => bool" |
62 |
59 |