2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-02 wenzelm 2014-03-02 more standard module name;
2014-03-02 wenzelm 2014-03-02 silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;
2014-03-02 wenzelm 2014-03-02 tuned whitespace;
2014-02-27 wenzelm 2014-02-27 tuned whitespace; modernized theory setup;
2014-02-15 wenzelm 2014-02-15 removed dead code; tuned;
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-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-11-27 wenzelm 2011-11-27 more antiquotations;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
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 antiquotations for remaining unqualified constants in HOL
2010-07-08 haftmann 2010-07-08 tuned titles
2010-05-25 wenzelm 2010-05-25 moved ML files where they are actually used; more precise dependencies;