src/HOL/ex/SAT_Examples.thy
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-05-04 blanchet 2014-05-04 tuned structure name
2014-05-04 blanchet 2014-05-04 renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
2014-05-01 boehmes 2014-05-01 added internal proof-producing SAT solver
2014-02-01 wenzelm 2014-02-01 proper config options; proper context for printing;
2014-02-01 wenzelm 2014-02-01 more standard file/module names;
2013-05-17 wenzelm 2013-05-17 proper option quick_and_dirty;
2013-03-05 webertj 2013-03-05 Avoid ML warning about unreferenced identifier.
2012-04-12 wenzelm 2012-04-12 more standard method setup;
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