changeset 55159 | 608c157d743d |
parent 54681 | 8a8e6db7f391 |
child 56410 | a14831ac3023 |
55158:39bcdf19dd14 | 55159:608c157d743d |
---|---|
3 *) |
3 *) |
4 |
4 |
5 header{* A formalization of formal power series *} |
5 header{* A formalization of formal power series *} |
6 |
6 |
7 theory Formal_Power_Series |
7 theory Formal_Power_Series |
8 imports Binomial |
8 imports "~~/src/HOL/Number_Theory/Binomial" |
9 begin |
9 begin |
10 |
10 |
11 |
11 |
12 subsection {* The type of formal power series*} |
12 subsection {* The type of formal power series*} |
13 |
13 |