src/HOL/Library/Formal_Power_Series.thy
changeset 30661 54858c8ad226
parent 30488 5c4c3a9e9102
child 30747 b8ca7e450de3
--- a/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      Formal_Power_Series.thy
-    ID:
     Author:     Amine Chaieb, University of Cambridge
 *)
 
 header{* A formalization of formal power series *}
 
 theory Formal_Power_Series
-  imports Main Fact Parity
+imports Main Fact Parity
 begin
 
 subsection {* The type of formal power series*}