src/HOL/Imperative_HOL/Heap.thy
changeset 77106 5ef443fa4a5d
parent 69597 ff784d5a5bfb
--- a/src/HOL/Imperative_HOL/Heap.thy	Fri Jan 27 16:52:39 2023 +0100
+++ b/src/HOL/Imperative_HOL/Heap.thy	Thu Jan 26 15:18:55 2023 +0100
@@ -79,9 +79,10 @@
   by (rule countable_classI [of addr_of_ref]) simp
 
 instance array :: (type) heap ..
+
 instance ref :: (type) heap ..
-    
-    
+
+
 text \<open>Syntactic convenience\<close>
 
 setup \<open>