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