--- a/src/HOL/Library/Polynomial_FPS.thy Mon Apr 03 23:31:31 2017 +0200
+++ b/src/HOL/Library/Polynomial_FPS.thy Tue Apr 04 11:52:28 2017 +0200
@@ -1,13 +1,13 @@
-(*
- File: Polynomial_FPS.thy
- Author: Manuel Eberl (TUM)
+(* Title: HOL/Library/Polynomial_FPS.thy
+ Author: Manuel Eberl, TU München
- Converting polynomials to formal power series
+Converting polynomials to formal power series.
*)
section \<open>Converting polynomials to formal power series\<close>
+
theory Polynomial_FPS
-imports Polynomial Formal_Power_Series
+ imports Polynomial Formal_Power_Series
begin
definition fps_of_poly where