# HG changeset patch
# User berghofe
# Date 1150125363 -7200
# Node ID ee5cd747c10afb52924c840f9a72dd49d1f630fd
# Parent  9c1732a66b0bc1bc39d1841206c4e78cc967f045
Added "evaluation" method.

diff -r 9c1732a66b0b -r ee5cd747c10a NEWS
--- a/NEWS	Mon Jun 12 15:58:12 2006 +0200
+++ b/NEWS	Mon Jun 12 17:16:03 2006 +0200
@@ -456,6 +456,10 @@
 * Library: added theory AssocList which implements (finite) maps as
 association lists.
 
+* New proof method "evaluation" for efficiently solving a goal
+  (i.e. a boolean expression) by compiling it to ML. The goal is
+  "proved" (via the oracle "Evaluation") if it evaluates to True.
+
 
 *** HOL-Complex ***