# HG changeset patch # User lammich # Date 1496328965 -7200 # Node ID 797ef48891773e5ffe0736c0c052a17209115e66 # Parent 5b2fab45db92d42b00ae5481df41dcb35d835a14 Added char, ref, array to heap-storable types diff -r 5b2fab45db92 -r 797ef4889177 src/HOL/Imperative_HOL/Heap.thy --- 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 \Syntactic convenience\ setup \