equal
deleted
inserted
replaced
26 |
26 |
27 instance option :: (heap) heap .. |
27 instance option :: (heap) heap .. |
28 |
28 |
29 instance int :: heap .. |
29 instance int :: heap .. |
30 |
30 |
31 instance message_string :: countable |
31 instance String.literal :: countable |
32 by (rule countable_classI [of "message_string_case to_nat"]) |
32 by (rule countable_classI [of "String.literal_case to_nat"]) |
33 (auto split: message_string.splits) |
33 (auto split: String.literal.splits) |
34 |
34 |
35 instance message_string :: heap .. |
35 instance String.literal :: heap .. |
36 |
36 |
37 text {* Reflected types themselves are heap-representable *} |
37 text {* Reflected types themselves are heap-representable *} |
38 |
38 |
39 instantiation typerep :: countable |
39 instantiation typerep :: countable |
40 begin |
40 begin |