equal
deleted
inserted
replaced
1 (* Title: Formal_Power_Series.thy |
1 (* Title: Formal_Power_Series.thy |
2 ID: |
|
3 Author: Amine Chaieb, University of Cambridge |
2 Author: Amine Chaieb, University of Cambridge |
4 *) |
3 *) |
5 |
4 |
6 header{* A formalization of formal power series *} |
5 header{* A formalization of formal power series *} |
7 |
6 |
8 theory Formal_Power_Series |
7 theory Formal_Power_Series |
9 imports Main Fact Parity |
8 imports Main Fact Parity |
10 begin |
9 begin |
11 |
10 |
12 subsection {* The type of formal power series*} |
11 subsection {* The type of formal power series*} |
13 |
12 |
14 typedef (open) 'a fps = "{f :: nat \<Rightarrow> 'a. True}" |
13 typedef (open) 'a fps = "{f :: nat \<Rightarrow> 'a. True}" |