src/HOL/SAT.thy
2012-10-31 blanchet 2012-10-31 moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
2012-10-31 blanchet 2012-10-31 moved Refute to "HOL/Library" to speed up building "Main" even more
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-01-03 blanchet 2012-01-03 tuned Refute
2010-09-02 blanchet 2010-09-02 use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine
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