# HG changeset patch
# User haftmann
# Date 1536394108 0
# Node ID a0b19a163f5ee3276006e878eb49d2ff9647b685
# Parent  cbf5475a0f66e5ecc11df16fdee4c9c58ca18c33
left-over rename from 3f9bb52082c4

diff -r cbf5475a0f66 -r a0b19a163f5e NEWS
--- a/NEWS	Fri Sep 07 23:48:19 2018 +0200
+++ b/NEWS	Sat Sep 08 08:08:28 2018 +0000
@@ -31,6 +31,10 @@
 * Sledgehammer: The URL for SystemOnTPTP, which is used by remote
 provers, has been updated.
 
+* Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap
+and prod_mset.swap, similarly to sum.swap and prod.swap.
+INCOMPATIBILITY.
+
 
 *** ML ***
 
diff -r cbf5475a0f66 -r a0b19a163f5e src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Sep 07 23:48:19 2018 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Sep 08 08:08:28 2018 +0000
@@ -2251,7 +2251,7 @@
     F (image_mset (g x) B) \<^bold>* F {#F {#g i j. i \<in># A#}. j \<in># B#}"
   by (induction B) (simp_all add: left_commute semigroup.assoc semigroup_axioms)
 
-lemma commute:
+lemma swap:
   "F (image_mset (\<lambda>i. F (image_mset (g i) B)) A) =
     F (image_mset (\<lambda>j. F (image_mset (\<lambda>i. g i j) A)) B)"
   apply (induction A, simp)
@@ -2348,7 +2348,7 @@
 lemma sum_mset_product:
   fixes f :: "'a::{comm_monoid_add,times} \<Rightarrow> 'b::semiring_0"
   shows "(\<Sum>i \<in># A. f i) * (\<Sum>i \<in># B. g i) = (\<Sum>i\<in>#A. \<Sum>j\<in>#B. f i * g j)"
-  by (subst sum_mset.commute) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
+  by (subst sum_mset.swap) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
 
 context semiring_1
 begin