Added "evaluation" method.

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