Added char, ref, array to heap-storable types
authorlammich <lammich@in.tum.de>
Thu, 01 Jun 2017 16:56:05 +0200
changeset 66004 797ef4889177
parent 66003 5b2fab45db92
child 66005 10e5265c2a25
Added char, ref, array to heap-storable types
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>