# HG changeset patch
# User desharna
# Date 1637838829 -3600
# Node ID 5749fefd3fa0b9b58e92809ba3269426f0c4aa9c
# Parent  825cd198d85cb8c7cb990b293fad48cb459aec7e
simplified mult_cancel_max and introduced orginal lemma as mult_cancel_max0

diff -r 825cd198d85c -r 5749fefd3fa0 NEWS
--- 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.
 
 
diff -r 825cd198d85c -r 5749fefd3fa0 src/HOL/Library/Multiset.thy
--- 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>