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