src/HOL/Semiring_Normalization.thy
20 months ago haftmann 2017-10-09 tuned imports
2015-09-10 wenzelm 2015-09-10 more standard local_theory operations; eliminated slightly odd @{cpat};
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2015-02-18 haftmann 2015-02-18 inlined rules to free user-space from technical names
2015-02-18 haftmann 2015-02-18 explicit declaration allows cumulative declaration
2015-02-15 haftmann 2015-02-15 deleted ineffective declarations
2015-02-15 haftmann 2015-02-15 dropped unused rules
2015-02-15 haftmann 2015-02-15 self-contained declaration attribute
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
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