src/HOL/Imperative_HOL/Heap.thy
changeset 66004 797ef4889177
parent 63167 0909deb8059b
child 66453 cc19f7ca2ed6
--- 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>