src/HOL/Tools/sat_funcs.ML
2009-07-27 ago moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-07-23 ago more @{theory} antiquotations;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-15 ago more antiquotations;
2008-12-31 ago moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-06-10 ago eliminated obsolete case_split_thm -- use case_split;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago cat_lines;
2008-05-17 ago structure Display: less pervasive operations;
2007-07-05 ago renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-03 ago Conjunction.intr/elim_balanced;
2007-05-10 ago moved conversions to structure Conv;
2006-12-11 ago ordered lists instead of tables for resolving hyps; speedup
2006-12-10 ago ML_Syntax.print_XXX;
2006-11-29 ago clauses sorted according to term order (significant speedup in some cases)
2006-11-23 ago renamed string_of_pair/list/option to ML_Syntax.str_of_pair/list/option;
2006-11-09 ago timing/tracing code removed
2006-11-09 ago interpreters for fst and snd added
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