equal
deleted
inserted
replaced
1 (* Title: HOL/Reflection/Approximation.thy |
1 (* Title: HOL/Reflection/Approximation.thy |
2 * Author: Johannes Hölzl <hoelzl@in.tum.de> 2008 / 2009 |
2 Author: Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009 |
3 *) |
3 *) |
|
4 |
4 header {* Prove unequations about real numbers by computation *} |
5 header {* Prove unequations about real numbers by computation *} |
|
6 |
5 theory Approximation |
7 theory Approximation |
6 imports Complex_Main Float Reflection Dense_Linear_Order Efficient_Nat |
8 imports Complex_Main Float Reflection Dense_Linear_Order Efficient_Nat |
7 begin |
9 begin |
8 |
10 |
9 section "Horner Scheme" |
11 section "Horner Scheme" |