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*}