--- a/NEWS Wed Sep 28 16:58:06 2005 +0200
+++ b/NEWS Wed Sep 28 18:50:42 2005 +0200
@@ -394,8 +394,9 @@
fragment of HOL, including axiomatic type classes, constdefs and
typedefs, inductive datatypes and recursion.
-* New tactic 'sat' to prove propositional tautologies. Requires
-zChaff with proof generation to be installed.
+* New tactics 'sat' and 'satx' to prove propositional tautologies.
+Requires zChaff with proof generation to be installed. See
+HOL/ex/SAT_Examples.thy for examples.
* Datatype induction via method 'induct' now preserves the name of the
induction variable. For example, when proving P(xs::'a list) by