| changeset 65435 | 378175f44328 |
| parent 65417 | fc41a5650fb1 |
| child 65578 | e4997c181cce |
| 65434:e62b1af601f0 | 65435:378175f44328 |
|---|---|
1 (* Title: HOL/Library/Formal_Power_Series.thy |
1 (* Title: HOL/Computational_Algebra/Formal_Power_Series.thy |
2 Author: Amine Chaieb, University of Cambridge |
2 Author: Amine Chaieb, University of Cambridge |
3 *) |
3 *) |
4 |
4 |
5 section \<open>A formalization of formal power series\<close> |
5 section \<open>A formalization of formal power series\<close> |
6 |
6 |