equal
deleted
inserted
replaced
8 imports Complex_Main Rat_Pair Polynomial_List |
8 imports Complex_Main Rat_Pair Polynomial_List |
9 begin |
9 begin |
10 |
10 |
11 subsection{* Datatype of polynomial expressions *} |
11 subsection{* Datatype of polynomial expressions *} |
12 |
12 |
13 datatype_new poly = C Num | Bound nat | Add poly poly | Sub poly poly |
13 datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly |
14 | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly |
14 | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly |
15 |
15 |
16 abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)" |
16 abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)" |
17 abbreviation poly_p :: "int \<Rightarrow> poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \<equiv> C (i)\<^sub>N" |
17 abbreviation poly_p :: "int \<Rightarrow> poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \<equiv> C (i)\<^sub>N" |
18 |
18 |