# HG changeset patch
# User desharna
# Date 1637839190 -3600
# Node ID b65336541c19a54c88e2abdef94eef9834c96556
# Parent  5749fefd3fa0b9b58e92809ba3269426f0c4aa9c
renamed multp_code_iff and multeqp_code_iff

diff -r 5749fefd3fa0 -r b65336541c19 NEWS
--- a/NEWS	Thu Nov 25 12:13:49 2021 +0100
+++ b/NEWS	Thu Nov 25 12:19:50 2021 +0100
@@ -14,6 +14,8 @@
     multeqp ~> multeqp_code
     multp_cancel_add_mset ~> multp_cancel_add_mset0
     multp_cancel_add_mset0[simplified] ~> multp_cancel_add_mset
+    multp_code_iff ~> multp_code_iff_mult
+    multeqp_code_iff ~> multeqp_code_iff_reflcl_mult
   Minor INCOMPATIBILITY.
 
 
diff -r 5749fefd3fa0 -r b65336541c19 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Nov 25 12:13:49 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Nov 25 12:19:50 2021 +0100
@@ -3079,7 +3079,7 @@
     (let Z = M \<inter># N; X = M - Z; Y = N - Z in
     (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x))"
 
-lemma multp_code_iff:
+lemma multp_code_iff_mult:
   assumes "irrefl R" and "trans R" and [simp]: "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
   shows "multp_code P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
 proof -
@@ -3100,7 +3100,7 @@
   qed
 qed
 
-lemma multeqp_code_iff:
+lemma multeqp_code_iff_reflcl_mult:
   assumes "irrefl R" and "trans R" and "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
   shows "multeqp_code P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
 proof -
@@ -3111,10 +3111,9 @@
   }
   then have "multeqp_code P N M \<longleftrightarrow> multp_code P N M \<or> N = M"
     by (auto simp: multeqp_code_def multp_code_def Let_def in_diff_count)
-  thus ?thesis using multp_code_iff[OF assms] by simp
+  thus ?thesis using multp_code_iff_mult[OF assms] by simp
 qed
 
-
 subsubsection \<open>Partial-order properties\<close>
 
 lemma (in preorder) mult1_lessE: