# HG changeset patch
# User wenzelm
# Date 1239201303 -7200
# Node ID dda08b76fa999333af77a2afa08aef09cbcd34d2
# Parent  a3cfe0e27debfc278696e02e580977f25d514527
updated official title of contribution by Johannes Hoelzl;

diff -r a3cfe0e27deb -r dda08b76fa99 CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Apr 07 23:25:50 2009 +0200
+++ b/CONTRIBUTORS	Wed Apr 08 16:35:03 2009 +0200
@@ -11,6 +11,10 @@
   Cambridge
   Elementary topology in Euclidean space.
 
+* March 2009: Johannes Hoelzl, TUM
+  Method "approximation", which proves real valued inequalities by
+  computation.
+
 * February 2009: Filip Maric, Univ. of Belgrade
   A Serbian theory.
 
diff -r a3cfe0e27deb -r dda08b76fa99 src/HOL/Decision_Procs/Approximation.thy
--- 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