equal
deleted
inserted
replaced
26 instance list :: (heap) heap .. |
26 instance list :: (heap) heap .. |
27 |
27 |
28 instance option :: (heap) heap .. |
28 instance option :: (heap) heap .. |
29 |
29 |
30 instance int :: heap .. |
30 instance int :: heap .. |
31 |
|
32 instance set :: ("{heap, finite}") heap .. |
|
33 |
31 |
34 instance message_string :: countable |
32 instance message_string :: countable |
35 by (rule countable_classI [of "message_string_case to_nat"]) |
33 by (rule countable_classI [of "message_string_case to_nat"]) |
36 (auto split: message_string.splits) |
34 (auto split: message_string.splits) |
37 |
35 |