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