--- 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)
--- 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
--- 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))"