2009-12-14 blanchet 2009-12-14 added "no_assms" option to Refute, and include structured proof assumptions by default; will do the same for Quickcheck unless there are objections
2009-07-27 wenzelm 2009-07-27 proper context for SAT tactics; eliminated METAHYPS; tuned signatures;
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2008-04-02 haftmann 2008-04-02 tuned imports
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2005-10-09 webertj 2005-10-09 Tactics sat and satx reimplemented, several improvements
2005-09-29 wenzelm 2005-09-29 explicit dependencies of SAT vs. Refute; removed unused methods;
2005-09-25 webertj 2005-09-25 sat_solver.ML not loaded anymore (already loaded by Refute.thy)
2005-09-24 webertj 2005-09-24 cnf_struct renamed to cnf
2005-09-24 obua 2005-09-24 preliminary fix of HOL build problem
2005-09-23 webertj 2005-09-23 new sat tactic imports resolution proofs from zChaff