src/HOL/Decision_Procs/Commutative_Ring.thy
2014-09-09 blanchet 2014-09-09 ported Decision_Procs to new datatypes
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-02-27 wenzelm 2014-02-27 tuned whitespace; tuned proofs;
2014-02-25 wenzelm 2014-02-25 tuned specifications and proofs;
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-07-15 wenzelm 2013-07-15 tuned specifications and proofs;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-12 wenzelm 2012-04-12 more standard method setup;
2011-02-21 wenzelm 2011-02-21 tuned proofs -- eliminated prems;
2010-10-24 nipkow 2010-10-24 nat_number -> eval_nat_numeral
2009-10-30 haftmann 2009-10-30 moved Commutative_Ring into session Decision_Procs