# HG changeset patch
# User desharna
# Date 1718047944 -7200
# Node ID a6d5de03ffeb0118b9d64a4ffdbccb8d72d0252d
# Parent  5e5dcebd1ed897bbf554d593aaf46e93d262b289
renamed lemmas

diff -r 5e5dcebd1ed8 -r a6d5de03ffeb NEWS
--- a/NEWS	Mon Jun 10 18:10:09 2024 +0200
+++ b/NEWS	Mon Jun 10 21:32:24 2024 +0200
@@ -29,6 +29,12 @@
       wfP_wf_eq ~> wfp_wf_eq
       wf_acc_iff ~> wf_iff_acc
 
+* Theory "HOL-Library.Multiset":
+  - Renamed lemmas. Minor INCOMPATIBILITY.
+      wfP_less_multiset ~> wfp_less_multiset
+      wfP_multp ~> wfp_multp
+      wfP_subset_mset ~> wfp_subset_mset
+
 
 New in Isabelle2024 (May 2024)
 ------------------------------
diff -r 5e5dcebd1ed8 -r a6d5de03ffeb src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Jun 10 18:10:09 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Jun 10 21:32:24 2024 +0200
@@ -1550,7 +1550,7 @@
 lemma wf_subset_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
   using mset_subset_size wfp_def wfp_if_convertible_to_nat by blast
 
-lemma wfP_subset_mset[simp]: "wfP (\<subset>#)"
+lemma wfp_subset_mset[simp]: "wfp (\<subset>#)"
   by (rule wf_subset_mset_rel[to_pred])
 
 lemma full_multiset_induct [case_names less]:
@@ -3245,7 +3245,7 @@
 lemma wf_mult: "wf r \<Longrightarrow> wf (mult r)"
   unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
 
-lemma wfP_multp: "wfP r \<Longrightarrow> wfP (multp r)"
+lemma wfp_multp: "wfp r \<Longrightarrow> wfp (multp r)"
   unfolding multp_def wfp_def
   by (simp add: wf_mult)
 
@@ -3694,11 +3694,11 @@
   shows "M < M \<Longrightarrow> R"
   by simp
 
-lemma wfP_less_multiset[simp]:
-  assumes wfP_less: "wfP ((<) :: ('a :: preorder) \<Rightarrow> 'a \<Rightarrow> bool)"
-  shows "wfP ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
+lemma wfp_less_multiset[simp]:
+  assumes wfp_less: "wfp ((<) :: ('a :: preorder) \<Rightarrow> 'a \<Rightarrow> bool)"
+  shows "wfp ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
   unfolding less_multiset_def
-  using wfP_multp[OF wfP_less] .
+  using wfp_multp[OF wfp_less] .
 
 
 subsubsection \<open>Strict total-order properties\<close>
diff -r 5e5dcebd1ed8 -r a6d5de03ffeb src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Mon Jun 10 18:10:09 2024 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Mon Jun 10 21:32:24 2024 +0200
@@ -819,7 +819,7 @@
   have "wfp ((<) :: 'a \<Rightarrow> 'a \<Rightarrow> bool)"
     using wfp_on_less .
   hence "wfp ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
-    unfolding less_multiset_def by (rule wfP_multp)
+    unfolding less_multiset_def by (rule wfp_multp)
   thus "(\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a"
     unfolding wfp_on_def[of UNIV, simplified] by metis
 qed