--- a/NEWS Thu Feb 05 11:45:15 2009 +0100
+++ b/NEWS Thu Feb 05 11:49:15 2009 +0100
@@ -197,7 +197,11 @@
are treated as expected by the 'class' command.
* Theory "Reflection" now resides in HOL/Library. Common reflection examples
-(Cooper, MIR, Ferrack) now in distinct session directory HOL/Reflection.
+(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.
* Entry point to Word library now simply named "Word". INCOMPATIBILITY.