diff -r ed09706ecc5d -r 72ad5f2a3803 NEWS
--- a/NEWS	Thu Mar 11 13:03:31 2004 +0100
+++ b/NEWS	Thu Mar 11 13:34:13 2004 +0100
@@ -139,6 +139,11 @@
 * ML: the legacy theory structures Int and List have been removed. They had
   conflicted with ML Basis Library structures having the same names.
 
+* 'refute' command added to search for (finite) countermodels.  Only works
+  for a fragment of HOL.  The installation of an external SAT solver is
+  highly recommended.  See "HOL/Refute.thy" for details.
+
+
 New in Isabelle2003 (May 2003)
 --------------------------------