src/HOL/Library/Polynomial_FPS.thy
changeset 65366 10ca63a18e56
parent 64911 f0e07600de47
--- 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