src/HOL/Tools/sat_funcs.ML
2007-07-05 wenzelm 2007-07-05 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-03 wenzelm 2007-07-03 Conjunction.intr/elim_balanced; CONVERSION tactical; tuned;
2007-05-10 wenzelm 2007-05-10 moved conversions to structure Conv;
2006-12-11 webertj 2006-12-11 ordered lists instead of tables for resolving hyps; speedup
2006-12-10 wenzelm 2006-12-10 ML_Syntax.print_XXX;
2006-11-29 webertj 2006-11-29 clauses sorted according to term order (significant speedup in some cases)
2006-11-23 wenzelm 2006-11-23 renamed string_of_pair/list/option to ML_Syntax.str_of_pair/list/option;
2006-11-09 webertj 2006-11-09 timing/tracing code removed
2006-11-09 webertj 2006-11-09 interpreters for fst and snd added
2006-09-06 webertj 2006-09-06 rawsat_thm: mk_conjunction_list replaced by Conjunction.mk_conjunction_list
2006-09-02 webertj 2006-09-02 tuned
2006-08-30 webertj 2006-08-30 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
2006-08-09 webertj 2006-08-09 tuned: string_of_list, string_of_pair
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-07-20 webertj 2006-07-20 comments fixed, member function renamed
2006-07-10 webertj 2006-07-10 minor optimization wrt. certifying terms
2006-07-07 webertj 2006-07-07 "solver" reference added to make the SAT solver configurable
2006-07-03 webertj 2006-07-03 comments fixed, minor optimization wrt. certifying terms
2006-05-03 webertj 2006-05-03 pre_cnf_tac: beta-eta-normalization restricted to the current subgoal
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-12 webertj 2005-10-12 counter added to SAT signature
2005-10-12 webertj 2005-10-12 no proof reconstruction when quick_and_dirty is set
2005-10-09 webertj 2005-10-09 Tactics sat and satx reimplemented, several improvements
2005-09-28 webertj 2005-09-28 pre_sat_tac moved towards end of file
2005-09-28 webertj 2005-09-28 comment fixed
2005-09-24 webertj 2005-09-24 replay_proof optimized: now performs backwards proof search
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