--- 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.
--- 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