src/HOL/Tools/sat_funcs.ML
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-05-17 wenzelm 2013-05-17 proper option quick_and_dirty;
2013-05-17 wenzelm 2013-05-17 tuned signature;
2013-03-27 wenzelm 2013-03-27 tuned;
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-08-08 wenzelm 2011-08-08 misc tuning -- eliminated old-fashioned rep_thm;
2011-01-10 wenzelm 2011-01-10 eliminated Int.toString;
2011-01-08 wenzelm 2011-01-08 modernized structure Prop_Logic; avoid ML structure aliases;
2011-01-07 wenzelm 2011-01-07 tuned whitespace, indentation, comments;
2010-10-28 wenzelm 2010-10-28 eliminated dead code;
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-10-27 wenzelm 2009-10-27 normalized basic type abbreviations;
2009-10-27 wenzelm 2009-10-27 more thread-safe access to global refs;
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-17 wenzelm 2009-10-17 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-08-28 wenzelm 2009-08-28 modernized messages -- eliminated ctyp/cterm operations;
2009-07-30 wenzelm 2009-07-30 qualified Subgoal.FOCUS;
2009-07-27 wenzelm 2009-07-27 proper context for SAT tactics; eliminated METAHYPS; tuned signatures;
2009-07-27 wenzelm 2009-07-27 moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-07-23 wenzelm 2009-07-23 more @{theory} antiquotations;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-06-10 wenzelm 2008-06-10 eliminated obsolete case_split_thm -- use case_split;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 cat_lines;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
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