src/HOL/Tools/groebner.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-11-04 haftmann 2013-11-04 dropped dead code
2013-06-27 wenzelm 2013-06-27 tuned signature;
2013-05-20 wenzelm 2013-05-20 proper run-time context;
2013-05-11 wenzelm 2013-05-11 prefer explicitly qualified exceptions, which is particular important for robust handlers;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-04-12 wenzelm 2012-04-12 more standard method setup;
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-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-01-07 wenzelm 2011-01-07 eliminated alias;
2011-01-07 wenzelm 2011-01-07 do not open ML structures;
2010-11-26 wenzelm 2010-11-26 eliminated some clones of eq_list;
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-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-05-07 haftmann 2010-05-07 delete Groebner_Basis directory -- only one file left