src/HOL/Decision_Procs/commutative_ring_tac.ML
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-04-22 nipkow 2015-04-22 added simp rules for ==>
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-10-09 haftmann 2014-10-09 more foundational definition for predicate even
2014-02-27 wenzelm 2014-02-27 tuned whitespace; tuned proofs;
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-27 wenzelm 2012-02-27 prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-07-08 haftmann 2010-07-08 tuned titles
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-11-04 nipkow 2009-11-04 merged
2009-10-30 haftmann 2009-10-30 moved Commutative_Ring into session Decision_Procs