src/HOL/Semiring_Normalization.thy
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2010-07-23 haftmann 2010-07-23 proper subclass instead of sublocale
2010-05-12 haftmann 2010-05-12 tuned proofs and fact and class names
2010-05-12 haftmann 2010-05-12 tuned fact collection names and some proofs
2010-05-12 haftmann 2010-05-12 grouped local statements
2010-05-11 hoelzl 2010-05-11 Add rules directly to the corresponding class locales instead.
2010-05-08 haftmann 2010-05-08 moved normalization proof tool infrastructure to canonical algebraic classes
2010-05-07 haftmann 2010-05-07 renamed Normalizer to the more specific Semiring_Normalizer
2010-05-07 haftmann 2010-05-07 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces