# 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_" 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;