Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
changeset 63594 bd218a9320b5
parent 63589 58aab4745e85 
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Aug 04 18:45:28 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Aug 04 19:36:31 2016 +0200
@@ -5,7 +5,7 @@
 theory Complex_Transcendental
 imports
   Complex_Analysis_Basics
-  Summation
+  Summation_Tests
 begin
 
 (* TODO: Figure out what to do with Möbius transformations *)
@@ -1647,7 +1647,7 @@
 
 lemma norm_powr_real_powr:
   "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
-  by (cases "w = 0") (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 
+  by (cases "w = 0") (auto simp add: norm_powr_real powr_def Im_Ln_eq_0
                                      complex_is_Real_iff in_Reals_norm complex_eq_iff)
 
 lemma tendsto_ln_complex [tendsto_intros]:
isabelle