# HG changeset patch
# User webertj
# Date 1153092497 -7200
# Node ID 8e92a8f9720b989a822a750ec9bdff062fe3dc30
# Parent  5a6b33268bb6484f18d0b0d99dc91359db0a0c03
support for MiniSat proof traces added

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;