| changeset 19855 | ee5cd747c10a |
| parent 19814 | faa698d46686 |
| child 19895 | cab56c949350 |
--- 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 ***