diff -r 5a6b33268bb6 -r 8e92a8f9720b NEWS
--- a/NEWS	Mon Jul 17 00:37:06 2006 +0200
+++ b/NEWS	Mon Jul 17 01:28:17 2006 +0200
@@ -477,6 +477,9 @@
 "=" on type bool) are handled, variable names of the form "lit_<n>"
 are no longer reserved, significant speedup.
 
+* Tactics 'sat' and 'satx' can now replay MiniSat proof traces.  zChaff is
+still supported as well.
+
 * inductive and datatype: provide projections of mutual rules, bundled
 as foo_bar.inducts;