# HG changeset patch
# User hoelzl
# Date 1233844506 -3600
# Node ID fa4ec7a7215c91a6293b8c6f14d7ca00bb9a34a0
# Parent  df25a6b1a4756bbd86f9981599d07f7a35140ef7
Updated NEWS about approximation

diff -r df25a6b1a475 -r fa4ec7a7215c NEWS
--- a/NEWS	Thu Feb 05 14:50:43 2009 +0100
+++ b/NEWS	Thu Feb 05 15:35:06 2009 +0100
@@ -200,8 +200,10 @@
 (Cooper, MIR, Ferrack, Approximation) now in distinct session directory
 HOL/Reflection. Here Approximation provides the new proof method
 "approximation". It proves formulas on real values by using interval arithmetic.
-In the formulas are also the transcendental functions sin, cos, tan, atan, ln
-and exp are allowed.
+In the formulas are also the transcendental functions sin, cos, tan, atan, ln,
+exp and the constant pi are allowed. For examples see
+src/HOL/ex/ApproximationEx.thy. To reach this the Leibnitz's Series for Pi and
+the arcus tangens and logarithm series is now proved in Isabelle.
 
 * Entry point to Word library now simply named "Word".  INCOMPATIBILITY.