src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
```     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Apr 20 13:46:36 2015 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Apr 21 17:19:00 2015 +0100
1.3 @@ -1263,9 +1263,6 @@
1.4
1.5  subsection{*Complex Powers*}
1.6
1.7 -lemma powr_0 [simp]: "0 powr z = 0"
1.8 -  by (simp add: powr_def)
1.9 -
1.10  lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
1.12
1.13 @@ -1526,7 +1523,7 @@
1.14  proof -
1.15    have nz0: "1 + \<i>*z \<noteq> 0"
1.16      using assms
1.17 -    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2)
1.18 +    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2)
1.19                less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
1.20    have "z \<noteq> -\<i>" using assms
1.21      by auto
1.22 @@ -1771,7 +1768,7 @@
1.23    by (blast intro: isCont_o2 [OF _ isCont_Arcsin])
1.24
1.25  lemma sin_Arcsin [simp]: "sin(Arcsin z) = z"
1.26 -proof -
1.27 +proof -
1.28    have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0"
1.29      by (simp add: algebra_simps)  --{*Cancelling a factor of 2*}
1.30    moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0"
1.31 @@ -1903,7 +1900,7 @@
1.32  proof (cases "Im z = 0")
1.33    case True
1.34    then show ?thesis
1.35 -    using assms
1.36 +    using assms
1.37      by (fastforce simp add: cmod_def Re_power2 Im_power2 algebra_simps abs_square_less_1 [symmetric])
1.38  next
1.39    case False
```