equal
deleted
inserted
replaced
2 Coercions removed by Dmitriy Traytel *) |
2 Coercions removed by Dmitriy Traytel *) |
3 |
3 |
4 header {* Prove Real Valued Inequalities by Computation *} |
4 header {* Prove Real Valued Inequalities by Computation *} |
5 |
5 |
6 theory Approximation |
6 theory Approximation |
7 imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat |
7 imports |
|
8 Complex_Main |
|
9 "~~/src/HOL/Library/Float" |
|
10 "~~/src/HOL/Library/Reflection" |
|
11 "~~/src/HOL/Decision_Procs/Dense_Linear_Order" |
|
12 "~~/src/HOL/Library/Efficient_Nat" |
8 begin |
13 begin |
9 |
14 |
10 section "Horner Scheme" |
15 section "Horner Scheme" |
11 |
16 |
12 subsection {* Define auxiliary helper @{text horner} function *} |
17 subsection {* Define auxiliary helper @{text horner} function *} |