diff -r 2e8f861d21d4 -r 07bec530f02e src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -612,7 +612,7 @@
   apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real Complex_eq)
   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib sin_squared_eq)
-  apply (simp add: power2_eq_square algebra_simps field_split_simps)
+  apply (simp add: power2_eq_square field_split_simps)
   done
 
 lemma norm_sin_squared:
@@ -621,7 +621,7 @@
   apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double Complex_eq)
   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib cos_squared_eq)
-  apply (simp add: power2_eq_square algebra_simps field_split_simps)
+  apply (simp add: power2_eq_square field_split_simps)
   done
 
 lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
@@ -1102,7 +1102,7 @@
   by auto
 
 lemma Arg2pi_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg2pi (cnj z) = Arg2pi (inverse z)"
-  apply (simp add: Arg2pi_eq_iff field_split_simps complex_norm_square [symmetric] mult.commute)
+  apply (simp add: Arg2pi_eq_iff field_split_simps complex_norm_square [symmetric])
   by (metis of_real_power zero_less_norm_iff zero_less_power)
 
 lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \<in> \<real> then Arg2pi z else 2*pi - Arg2pi z)"
@@ -1946,7 +1946,7 @@
   by (metis Arg_eq_0 Arg_inverse inverse_inverse_eq)
 
 lemma Arg_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg (cnj z) = Arg (inverse z)"
-  apply (simp add: Arg_eq_iff field_split_simps complex_norm_square [symmetric] mult.commute)
+  apply (simp add: Arg_eq_iff field_split_simps complex_norm_square [symmetric])
   by (metis of_real_power zero_less_norm_iff zero_less_power)
 
 lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> then Arg z else - Arg z)"
@@ -2936,7 +2936,7 @@
     unfolding Arctan_def scaleR_conv_of_real
     apply (intro derivative_eq_intros | simp add: nz0 *)+
     using nz0 nz1 zz
-    apply (simp add: algebra_simps field_split_simps power2_eq_square)
+    apply (simp add: field_split_simps power2_eq_square)
     apply algebra
     done
 qed
@@ -3014,7 +3014,7 @@
   have "\<exists>c. \<forall>u\<in>ball 0 1. Arctan u - G u = c"
   proof (rule has_field_derivative_zero_constant)
     fix u :: complex assume "u \<in> ball 0 1"
-    hence u: "norm u < 1" by (simp add: dist_0_norm)
+    hence u: "norm u < 1" by (simp)
     define K where "K = (norm u + 1) / 2"
     from u and abs_Im_le_cmod[of u] have Im_u: "\<bar>Im u\<bar> < 1" by linarith
     from u have K: "0 \<le> K" "norm u < K" "K < 1" by (simp_all add: K_def)
@@ -3634,7 +3634,7 @@
   assumes "z\<^sup>2 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0"
 proof -
   have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = z\<^sup>2 * (z\<^sup>2 - 1)"
-    by (simp add: power_mult_distrib algebra_simps)
+    by (simp add: algebra_simps)
   have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> z\<^sup>2 - 1"
   proof
     assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = z\<^sup>2 - 1"
@@ -3665,7 +3665,7 @@
   assumes "z\<^sup>2 \<noteq> 1" shows "sin(Arccos z) \<noteq> 0"
 proof -
   have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = -(z\<^sup>2) * (1 - z\<^sup>2)"
-    by (simp add: power_mult_distrib algebra_simps)
+    by (simp add: algebra_simps)
   have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1 - z\<^sup>2"
   proof
     assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = 1 - z\<^sup>2"
@@ -3971,7 +3971,7 @@
     shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n)^n = 1"
 proof -
   have *: "of_nat j * (complex_of_real pi * 2) = complex_of_real (2 * real j * pi)"
-    by (simp add: of_real_numeral)
+    by (simp)
   then show ?thesis
     apply (simp add: exp_of_nat_mult [symmetric] mult_ac exp_Euler)
     apply (simp only: * cos_of_real sin_of_real)
@@ -4006,7 +4006,7 @@
    note * = this
   show ?thesis
     using assms
-    by (simp add: exp_eq field_split_simps mult_ac of_real_numeral *)
+    by (simp add: exp_eq field_split_simps *)
 qed
 
 corollary bij_betw_roots_unity: