# HG changeset patch
# User webertj
# Date 1127510939 -7200
# Node ID 026f7bbc8a0f37932c3518909deb67c1d15c9856
# Parent  1330157e156a0bc975e0dc322e78b450efe71508
new sat tactic

diff -r 1330157e156a -r 026f7bbc8a0f NEWS
--- a/NEWS	Fri Sep 23 22:58:50 2005 +0200
+++ b/NEWS	Fri Sep 23 23:28:59 2005 +0200
@@ -392,6 +392,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.
+
 * Datatype induction via method 'induct' now preserves the name of the
 induction variable. For example, when proving P(xs::'a list) by
 induction on xs, the induction step is now P(xs) ==> P(a#xs) rather