| changeset 69517 | dc20f278e8f3 |
| parent 68721 | 53ad5c01be3f |
| child 69597 | ff784d5a5bfb |
--- a/src/HOL/Analysis/FPS_Convergence.thy Thu Dec 27 23:38:55 2018 +0100 +++ b/src/HOL/Analysis/FPS_Convergence.thy Fri Dec 28 10:29:59 2018 +0100 @@ -5,7 +5,8 @@ Connection of formal power series and actual convergent power series on Banach spaces (most notably the complex numbers). *) -section \<open>Convergence of formal power series\<close> +section \<open>Convergence of Formal Power Series\<close> + theory FPS_Convergence imports Conformal_Mappings