author | berghofe |
Wed, 07 May 2008 10:59:32 +0200 | |
changeset 26817 | 9217577e0a23 |
parent 26816 | e82229ee8f43 |
child 26818 | b4a24433154e |
--- a/src/HOL/Library/Heap.thy Wed May 07 10:59:29 2008 +0200 +++ b/src/HOL/Library/Heap.thy Wed May 07 10:59:32 2008 +0200 @@ -29,8 +29,6 @@ instance int :: heap .. -instance set :: ("{heap, finite}") heap .. - instance message_string :: countable by (rule countable_classI [of "message_string_case to_nat"]) (auto split: message_string.splits)