# HG changeset patch
# User lammich <lammich@in.tum.de>
# 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 \<open>Syntactic convenience\<close>
 
 setup \<open>