left-over rename from 3f9bb52082c4
authorhaftmann
Sat Sep 08 08:08:28 2018 +0000 (14 months ago ago)
changeset 68938a0b19a163f5e
parent 68937 cbf5475a0f66
child 68939 bcce5967e10e
left-over rename from 3f9bb52082c4
NEWS
src/HOL/Library/Multiset.thy
     1.1 --- a/NEWS	Fri Sep 07 23:48:19 2018 +0200
     1.2 +++ b/NEWS	Sat Sep 08 08:08:28 2018 +0000
     1.3 @@ -31,6 +31,10 @@
     1.4  * Sledgehammer: The URL for SystemOnTPTP, which is used by remote
     1.5  provers, has been updated.
     1.6  
     1.7 +* Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap
     1.8 +and prod_mset.swap, similarly to sum.swap and prod.swap.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  
    1.12  *** ML ***
    1.13  
     2.1 --- a/src/HOL/Library/Multiset.thy	Fri Sep 07 23:48:19 2018 +0200
     2.2 +++ b/src/HOL/Library/Multiset.thy	Sat Sep 08 08:08:28 2018 +0000
     2.3 @@ -2251,7 +2251,7 @@
     2.4      F (image_mset (g x) B) \<^bold>* F {#F {#g i j. i \<in># A#}. j \<in># B#}"
     2.5    by (induction B) (simp_all add: left_commute semigroup.assoc semigroup_axioms)
     2.6  
     2.7 -lemma commute:
     2.8 +lemma swap:
     2.9    "F (image_mset (\<lambda>i. F (image_mset (g i) B)) A) =
    2.10      F (image_mset (\<lambda>j. F (image_mset (\<lambda>i. g i j) A)) B)"
    2.11    apply (induction A, simp)
    2.12 @@ -2348,7 +2348,7 @@
    2.13  lemma sum_mset_product:
    2.14    fixes f :: "'a::{comm_monoid_add,times} \<Rightarrow> 'b::semiring_0"
    2.15    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)"
    2.16 -  by (subst sum_mset.commute) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
    2.17 +  by (subst sum_mset.swap) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
    2.18  
    2.19  context semiring_1
    2.20  begin