diff -r 99831590def5 -r b66788d19c0f NEWS
--- a/NEWS	Wed Nov 12 17:37:43 2014 +0100
+++ b/NEWS	Wed Nov 12 17:37:44 2014 +0100
@@ -168,6 +168,15 @@
 The "sos_cert" functionality is invoked as "sos" with additional
 argument. Minor INCOMPATIBILITY.
 
+* HOL-Decision_Procs:
+  - New counterexample generator quickcheck[approximation] for
+    inequalities of transcendental functions.
+    Uses hardware floating point arithmetic to randomly discover
+    potential counterexamples. Counterexamples are certified with the
+    'approximation' method.
+    See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
+    examples.
+
 
 *** Document preparation ***