author | webertj |
Mon, 17 Jul 2006 01:28:17 +0200 | |
changeset 20136 | 8e92a8f9720b |
parent 20135 | 5a6b33268bb6 |
child 20137 | 6c04453ac1bd |
--- 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;