diff -r d32e702d7ab8 -r 10ca63a18e56 src/HOL/Library/Polynomial_FPS.thy --- 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 \Converting polynomials to formal power series\ + theory Polynomial_FPS -imports Polynomial Formal_Power_Series + imports Polynomial Formal_Power_Series begin definition fps_of_poly where