--- 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
--- 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>