--- a/NEWS Sat Jan 28 22:29:24 2023 +0100
+++ b/NEWS Sat Jan 28 22:31:40 2023 +0100
@@ -215,6 +215,7 @@
* Theory "HOL-Library.Multiset_Order":
- Added lemmas.
irreflp_on_multpHO[simp]
+ multpHO_plus_plus[simp]
totalp_multpDM
totalp_multpHO
totalp_on_multpDM
--- a/src/HOL/Imperative_HOL/Array.thy Sat Jan 28 22:29:24 2023 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy Sat Jan 28 22:31:40 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 Sat Jan 28 22:29:24 2023 +0100
+++ b/src/HOL/Imperative_HOL/Heap.thy Sat Jan 28 22:31:40 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>
--- a/src/HOL/Library/Monad_Syntax.thy Sat Jan 28 22:29:24 2023 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy Sat Jan 28 22:31:40 2023 +0100
@@ -11,7 +11,7 @@
text \<open>
We provide a convenient do-notation for monadic expressions well-known from Haskell.
-const>\<open>Let\<close> is printed specially in do-expressions.
+\<^const>\<open>Let\<close> is printed specially in do-expressions.
\<close>
consts
--- a/src/HOL/Library/Multiset_Order.thy Sat Jan 28 22:29:24 2023 +0100
+++ b/src/HOL/Library/Multiset_Order.thy Sat Jan 28 22:31:40 2023 +0100
@@ -138,6 +138,9 @@
using multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M[THEN multp\<^sub>D\<^sub>M_imp_multp] multp_imp_multp\<^sub>H\<^sub>O
by blast
+lemma multp\<^sub>H\<^sub>O_plus_plus[simp]: "multp\<^sub>H\<^sub>O R (M + M1) (M + M2) \<longleftrightarrow> multp\<^sub>H\<^sub>O R M1 M2"
+ unfolding multp\<^sub>H\<^sub>O_def by simp
+
subsubsection \<open>Properties of Preorders\<close>