src/HOL/Tools/cnf_funcs.ML
2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-03 ago minor tuning of Thm.strip_shyps -- no longer pervasive;
2009-10-21 ago standardized basic operations on type option;
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-30 ago qualified Subgoal.FOCUS;
2009-07-27 ago proper context for SAT tactics;
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-03-20 ago eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2008-12-31 ago moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-03-19 ago avoid Auto_tac;
2007-10-11 ago rationalized redundant code
2006-11-29 ago simplified Logic.count_prems;
2006-09-15 ago tuned;
2006-08-30 ago faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
2006-03-10 ago clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
2005-10-09 ago Tactics sat and satx reimplemented, several improvements
2005-09-23 ago new sat tactic imports resolution proofs from zChaff