src/HOL/Tools/cnf_funcs.ML
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
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-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-03-19 wenzelm 2008-03-19 avoid Auto_tac;
2007-10-11 paulson 2007-10-11 rationalized redundant code
2006-11-29 wenzelm 2006-11-29 simplified Logic.count_prems;
2006-09-15 wenzelm 2006-09-15 tuned;
2006-08-30 webertj 2006-08-30 faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
2006-03-10 webertj 2006-03-10 clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
2005-10-09 webertj 2005-10-09 Tactics sat and satx reimplemented, several improvements
2005-09-23 webertj 2005-09-23 new sat tactic imports resolution proofs from zChaff