# HG changeset patch
# User haftmann
# Date 1674742735 -3600
# Node ID 5ef443fa4a5df356d8b668e256090f4b5a35c746
# Parent  bbe33afcfe1edee51ddd7f4e11992f2e5db392cf
tuned whitespace

diff -r bbe33afcfe1e -r 5ef443fa4a5d src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Fri Jan 27 16:52:39 2023 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy	Thu Jan 26 15:18:55 2023 +0100
@@ -450,7 +450,7 @@
 code_printing constant Array.nth' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.sub/ ((_),/ IntInf.toInt _))"
 code_printing constant Array.upd' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.update/ ((_),/ IntInf.toInt _,/ (_)))"
 code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
-  
+
 code_reserved SML Array
 
 
diff -r bbe33afcfe1e -r 5ef443fa4a5d src/HOL/Imperative_HOL/Heap.thy
--- 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>