changeset 77106 | 5ef443fa4a5d |
parent 69597 | ff784d5a5bfb |
--- a/src/HOL/Imperative_HOL/Heap.thy Fri Jan 27 16:52:39 2023 +0100 +++ b/src/HOL/Imperative_HOL/Heap.thy Thu Jan 26 15:18:55 2023 +0100 @@ -79,9 +79,10 @@ by (rule countable_classI [of addr_of_ref]) simp instance array :: (type) heap .. + instance ref :: (type) heap .. - - + + text \<open>Syntactic convenience\<close> setup \<open>