1.1 --- a/CONTRIBUTORS	Tue Apr 07 23:25:50 2009 +0200
     1.2 +++ b/CONTRIBUTORS	Wed Apr 08 16:35:03 2009 +0200
     1.3 @@ -11,6 +11,10 @@
     1.4    Cambridge
     1.5    Elementary topology in Euclidean space.
     1.6  
     1.7 +* March 2009: Johannes Hoelzl, TUM
     1.8 +  Method "approximation", which proves real valued inequalities by
     1.9 +  computation.
    1.10 +
    1.11  * February 2009: Filip Maric, Univ. of Belgrade
    1.12    A Serbian theory.
    1.13  

     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Apr 07 23:25:50 2009 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 08 16:35:03 2009 +0200
     2.3 @@ -1,6 +1,6 @@
     2.4  (* Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009 *)
     2.5  
     2.6 -header {* Prove unequations about real numbers by computation *}
     2.7 +header {* Prove Real Valued Inequalities by Computation *}
     2.8  
     2.9  theory Approximation
    2.10  imports Complex_Main Float Reflection Dense_Linear_Order Efficient_Nat