src/HOL/Tools/cnf_funcs.ML
2011-11-15 blanchet 2011-11-15 continued implementation of lambda-lifting in Metis
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-14 blanchet 2011-04-14 experiment with definitional CNF
2011-01-07 wenzelm 2011-01-07 tuned whitespace, indentation, comments;
2010-09-02 blanchet 2010-09-02 make definitional CNF translation code more robust in the presence of existential quantifiers in the "literals"
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use HOLogic.boolT and @{typ bool} more pervasively
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-05 haftmann 2010-05-05 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 wenzelm 2010-05-03 minor tuning of Thm.strip_shyps -- no longer pervasive;
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