new sat tactic
authorwebertj
Fri Sep 23 23:28:59 2005 +0200 (2005-09-23)
changeset 17619026f7bbc8a0f
parent 17618 1330157e156a
child 17620 49568e5e0450
new sat tactic
NEWS
     1.1 --- a/NEWS	Fri Sep 23 22:58:50 2005 +0200
     1.2 +++ b/NEWS	Fri Sep 23 23:28:59 2005 +0200
     1.3 @@ -392,6 +392,9 @@
     1.4  fragment of HOL, including axiomatic type classes, constdefs and
     1.5  typedefs, inductive datatypes and recursion.
     1.6  
     1.7 +* New tactic 'sat' to prove propositional tautologies.  Requires
     1.8 +zChaff with proof generation to be installed.
     1.9 +
    1.10  * Datatype induction via method 'induct' now preserves the name of the
    1.11  induction variable. For example, when proving P(xs::'a list) by
    1.12  induction on xs, the induction step is now P(xs) ==> P(a#xs) rather