src/HOL/Tools/sat_funcs.ML
2006-09-06 ago rawsat_thm: mk_conjunction_list replaced by Conjunction.mk_conjunction_list
2006-09-02 ago tuned
2006-08-30 ago faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
2006-08-09 ago tuned: string_of_list, string_of_pair
2006-08-02 ago proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
2006-07-20 ago comments fixed, member function renamed
2006-07-10 ago minor optimization wrt. certifying terms
2006-07-07 ago "solver" reference added to make the SAT solver configurable
2006-07-03 ago comments fixed, minor optimization wrt. certifying terms
2006-05-03 ago pre_cnf_tac: beta-eta-normalization restricted to the current subgoal
2006-05-02 ago beta_eta_conversion added to pre_cnf_tac
2006-03-10 ago clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
2005-10-12 ago counter added to SAT signature
2005-10-12 ago no proof reconstruction when quick_and_dirty is set
2005-10-09 ago Tactics sat and satx reimplemented, several improvements
2005-09-28 ago pre_sat_tac moved towards end of file
2005-09-28 ago comment fixed
2005-09-24 ago replay_proof optimized: now performs backwards proof search
2005-09-24 ago code reformatted and restructured, many minor modifications
2005-09-23 ago new sat tactic imports resolution proofs from zChaff