src/HOL/ex/SAT_Examples.thy
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