equal
deleted
inserted
replaced
6 Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 |
6 Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 |
7 *) |
7 *) |
8 |
8 |
9 header{*Univariate Real Polynomials*} |
9 header{*Univariate Real Polynomials*} |
10 |
10 |
11 theory Poly = Transcendental: |
11 theory Poly |
12 |
12 import Transcendental |
|
13 begin |
13 |
14 |
14 text{*Application of polynomial as a real function.*} |
15 text{*Application of polynomial as a real function.*} |
15 |
16 |
16 consts poly :: "real list => real => real" |
17 consts poly :: "real list => real => real" |
17 primrec |
18 primrec |