| changeset 30886 | dda08b76fa99 |
| parent 30549 | d2d7874648bd |
| child 30952 | 7ab2716dd93b |
--- a/src/HOL/Decision_Procs/Approximation.thy Tue Apr 07 23:25:50 2009 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Wed Apr 08 16:35:03 2009 +0200 @@ -1,6 +1,6 @@ (* Author: Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009 *) -header {* Prove unequations about real numbers by computation *} +header {* Prove Real Valued Inequalities by Computation *} theory Approximation imports Complex_Main Float Reflection Dense_Linear_Order Efficient_Nat