# HG changeset patch
# User webertj
# Date 1127926242 -7200
# Node ID ac97a91d557228f75f60674a00580a9f0d76c730
# Parent  04d51df0c328cdfa7e5971a89f1714fb2bdcd76b
pointer to HOL/ex/SAT_Examples.thy added

diff -r 04d51df0c328 -r ac97a91d5572 NEWS
--- 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