--- a/NEWS Thu Nov 25 11:33:38 2021 +0100
+++ b/NEWS Thu Nov 25 12:13:49 2021 +0100
@@ -9,9 +9,11 @@
*** HOL ***
-* Theory "HOL-Library.Multiset": consolidated operation and fact namesd
+* Theory "HOL-Library.Multiset": consolidated operation and fact names
multp ~> multp_code
multeqp ~> multeqp_code
+ multp_cancel_add_mset ~> multp_cancel_add_mset0
+ multp_cancel_add_mset0[simplified] ~> multp_cancel_add_mset
Minor INCOMPATIBILITY.
--- a/src/HOL/Library/Multiset.thy Thu Nov 25 11:33:38 2021 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Nov 25 12:13:49 2021 +0100
@@ -3049,7 +3049,7 @@
lemmas mult_cancel_add_mset =
mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral]
-lemma mult_cancel_max:
+lemma mult_cancel_max0:
assumes "trans s" and "irrefl s"
shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
proof -
@@ -3057,6 +3057,8 @@
thus ?thesis using mult_cancel[OF assms, of "X - X \<inter># Y" "X \<inter># Y" "Y - X \<inter># Y"] by auto
qed
+lemmas mult_cancel_max = mult_cancel_max0[simplified]
+
subsection \<open>Quasi-executable version of the multiset extension\<close>