author | lammich <lammich@in.tum.de> |
Thu, 01 Jun 2017 16:56:05 +0200 | |
changeset 66004 | 797ef4889177 |
parent 66003 | 5b2fab45db92 |
child 66005 | 10e5265c2a25 |
--- a/src/HOL/Imperative_HOL/Heap.thy Thu Jun 01 16:55:32 2017 +0200 +++ b/src/HOL/Imperative_HOL/Heap.thy Thu Jun 01 16:56:05 2017 +0200 @@ -32,6 +32,8 @@ instance String.literal :: heap .. +instance char :: heap .. + instance typerep :: heap .. @@ -76,6 +78,10 @@ instance ref :: (type) countable by (rule countable_classI [of addr_of_ref]) simp +instance array :: (type) heap .. +instance ref :: (type) heap .. + + text \<open>Syntactic convenience\<close> setup \<open>