| changeset 20136 | 8e92a8f9720b |
| parent 20118 | 0c1ec587a5a8 |
| child 20169 | 52173f7687fd |
--- 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;