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.