# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1554934336 -3600
# Node ID 089c1751479478e9dada9d01455c456cd29c321a
# Parent  c8deb8ba6d05321bb7c4e30a233713f42a310189
prod/sum fixes

diff -r c8deb8ba6d05 -r 089c17514794 src/HOL/Analysis/ex/Approximations.thy
--- a/src/HOL/Analysis/ex/Approximations.thy	Wed Apr 10 21:29:32 2019 +0100
+++ b/src/HOL/Analysis/ex/Approximations.thy	Wed Apr 10 23:12:16 2019 +0100
@@ -199,7 +199,7 @@
 lemma euler_approx_aux_Suc:
   "euler_approx_aux (Suc m) = 1 + Suc m * euler_approx_aux m"
   unfolding euler_approx_aux_def
-  by (subst sum_distrib_left) (simp add: atLeastAtMostSuc_conv)
+  by (subst sum_distrib_left) (simp add: atLeastAtMostSuc_conv mult.commute)
 
 lemma eval_euler_approx_aux:
   "euler_approx_aux 0 = 1"
@@ -209,7 +209,7 @@
 proof -
   have A: "euler_approx_aux (Suc m) = 1 + Suc m * euler_approx_aux m" for m :: nat
     unfolding euler_approx_aux_def
-    by (subst sum_distrib_left) (simp add: atLeastAtMostSuc_conv)
+    by (subst sum_distrib_left) (simp add: atLeastAtMostSuc_conv mult.commute)
   show ?th by (subst numeral_eq_Suc, subst A, subst numeral_eq_Suc [symmetric]) simp
 qed (simp_all add: euler_approx_aux_def)
 
diff -r c8deb8ba6d05 -r 089c17514794 src/HOL/Homology/Invariance_of_Domain.thy
--- a/src/HOL/Homology/Invariance_of_Domain.thy	Wed Apr 10 21:29:32 2019 +0100
+++ b/src/HOL/Homology/Invariance_of_Domain.thy	Wed Apr 10 23:12:16 2019 +0100
@@ -1,7 +1,7 @@
 section\<open>Invariance of Domain\<close>
 
 theory Invariance_of_Domain
-  imports Brouwer_Degree "HOL-Analysis.Continuous_Extension" "HOL-Analysis.Homeomorphism" 
+  imports Brouwer_Degree "HOL-Analysis.Continuous_Extension" "HOL-Analysis.Homeomorphism"
 
 begin
 
@@ -2065,8 +2065,7 @@
 qed
 
 
-
-subsection\<open> Invariance of dimension and domain in setting of R^n.\<close>
+subsection\<open> Invariance of dimension and domain\<close>
 
 lemma homeomorphic_maps_iff_homeomorphism [simp]:
    "homeomorphic_maps (top_of_set S) (top_of_set T) f g \<longleftrightarrow> homeomorphism S T f g"
@@ -2971,4 +2970,4 @@
     using not_less by blast
 qed
 
-end
\ No newline at end of file
+end
diff -r c8deb8ba6d05 -r 089c17514794 src/HOL/ex/Sum_of_Powers.thy
--- a/src/HOL/ex/Sum_of_Powers.thy	Wed Apr 10 21:29:32 2019 +0100
+++ b/src/HOL/ex/Sum_of_Powers.thy	Wed Apr 10 23:12:16 2019 +0100
@@ -24,7 +24,7 @@
   case (Suc l)
   have "of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
     using prod.atLeast0_lessThan_Suc [where ?'a = 'a, symmetric, of "\<lambda>i. of_nat (Suc n - i)" k]
-    by (simp add: ac_simps prod.atLeast0_lessThan_Suc_shift)
+    by (simp add: ac_simps prod.atLeast0_lessThan_Suc_shift del: prod.op_ivl_Suc)
   also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (Suc n - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
     by (simp add: Suc atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
   also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"