# HG changeset patch # User haftmann # Date 1281703396 -7200 # Node ID 721b4d6095b751363f98084de83f6e72a034796c # Parent 0dbbb511634df522ec7335eb141ec254ab802477 unit and bool are instances of heap diff -r 0dbbb511634d -r 721b4d6095b7 src/HOL/Imperative_HOL/Heap.thy --- a/src/HOL/Imperative_HOL/Heap.thy Fri Aug 13 14:41:27 2010 +0200 +++ b/src/HOL/Imperative_HOL/Heap.thy Fri Aug 13 14:43:16 2010 +0200 @@ -14,6 +14,10 @@ class heap = typerep + countable +instance unit :: heap .. + +instance bool :: heap .. + instance nat :: heap .. instance prod :: (heap, heap) heap ..