src/HOL/Decision_Procs/Polynomial_List.thy
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-19 hoelzl 2016-02-19 generalize more theorems to support enat and ennreal
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-07-09 wenzelm 2015-07-09 tuned proofs;
2015-06-20 wenzelm 2015-06-20 eliminated list_all;
2015-06-20 wenzelm 2015-06-20 tuned proofs;
2015-06-20 wenzelm 2015-06-20 isabelle update_cartouches;
2015-03-25 wenzelm 2015-03-25 prefer local fixes;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-10-31 haftmann 2013-10-31 consolidated clone theory
2013-08-06 wenzelm 2013-08-06 misc tuning and simplification;
2013-07-29 wenzelm 2013-07-29 tuned proofs;
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-08 haftmann 2010-09-08 modernized primrec
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-06-28 haftmann 2010-06-28 explicit is better than implicit
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-10-28 wenzelm 2009-10-28 eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-25 chaieb 2009-10-25 A theory of polynomials based on lists