2011-03-20 wenzelm 2011-03-20 structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
2011-01-08 wenzelm 2011-01-08 modernized structure Prop_Logic; avoid ML structure aliases;
2010-08-27 wenzelm 2010-08-27 expanded some aliases from structure Unsynchronized;
2010-08-17 webertj 2010-08-17 Tuned.
2009-11-07 webertj 2009-11-07 Due to popular demand: added a function that benchmarks proof reconstruction for a single DIMACS CNF file.
2009-10-17 wenzelm 2009-10-17 Unsynchronized.set etc.;
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;
2007-07-06 webertj 2007-07-06 cosmetic (line length fixed)
2007-01-10 webertj 2007-01-10 minor comment change
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-11-19 webertj 2006-11-19 profiling disabled
2006-08-30 webertj 2006-08-30 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
2006-08-02 webertj 2006-08-02 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
2006-08-01 webertj 2006-08-01 comment (timing information for last example) added
2006-07-17 webertj 2006-07-17 support for MiniSat proof traces added
2006-07-07 webertj 2006-07-07 "solver" reference added to make the SAT solver configurable
2006-07-03 webertj 2006-07-03 CNF tactic invocations moved into comments
2006-05-02 webertj 2006-05-02 beta_eta_conversion added to pre_cnf_tac
2006-03-10 webertj 2006-03-10 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
2005-10-09 webertj 2005-10-09 Tactics sat and satx reimplemented, several improvements
2005-09-24 webertj 2005-09-24 code reformatted and restructured, many minor modifications
2005-09-23 webertj 2005-09-23 new sat tactic imports resolution proofs from zChaff