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