src/HOL/Library/Polynomial.thy
2017-01-10 haftmann 2017-01-10 separate instance for semidom_modulo
2017-01-09 haftmann 2017-01-09 generalized definition
2017-01-09 haftmann 2017-01-09 moved some lemmas to appropriate places
2017-01-09 haftmann 2017-01-09 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
2017-01-07 haftmann 2017-01-07 obsolete
2017-01-05 haftmann 2017-01-05 tuned structure
2017-01-05 haftmann 2017-01-05 lead_coeff is more appropriate as abbreviation
2017-01-05 haftmann 2017-01-05 more lemmas; tuned headings
2016-12-22 haftmann 2016-12-22 more uniform div/mod relations
2016-12-17 haftmann 2016-12-17 more fine-grained type class hierarchy for div and mod
2016-12-17 haftmann 2016-12-17 restructured matter on polynomials and normalized fractions
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-26 haftmann 2016-09-26 syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div
2016-09-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-09-15 nipkow 2016-09-15 renamed listsum -> sum_list, listprod ~> prod_list
2016-08-10 wenzelm 2016-08-10 tuned proofs;
2016-07-13 eberlm 2016-07-13 Reformed factorial rings
2016-07-11 wenzelm 2016-07-11 tuned;
2016-06-16 eberlm 2016-06-16 Various additions to polynomials, FPSs, Gamma function
2016-05-25 wenzelm 2016-05-25 isabelle update_cartouches -c -t;
2016-04-26 wenzelm 2016-04-26 some uses of 'obtain' with structure statement;
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-04-20 Rene Thiemann 2016-04-20 fixed code equation for pdivmod, added improved code equation for pseudo_mod
2016-04-20 wenzelm 2016-04-20 proper latex;
2016-04-15 Rene Thiemann 2016-04-15 several updates on polynomial long division and pseudo division - division of polynomials is now available on idom_divide (was field before) - added polynomial pseudo division (on comm_ring_1) - improved code equation for polynomial (pseudo)-division (joint work of S. Joosten, R. Thiemann, and A. Yamada)
2016-02-25 eberlm 2016-02-25 Tuned Euclidean rings
2016-02-17 haftmann 2016-02-17 separated potentially conflicting type class instance into separate theory
2016-02-17 haftmann 2016-02-17 gcd instances for poly
2016-01-11 eberlm 2016-01-11 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
2016-01-05 wenzelm 2016-01-05 isabelle update_cartouches -c -t;
2016-01-05 eberlm 2016-01-05 Fixed sectioning in HOL/Library/Polynomial
2016-01-05 eberlm 2016-01-05 Added some facts about polynomials
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-09-24 wenzelm 2015-09-24 explicit indication of overloaded typedefs;
2015-07-08 haftmann 2015-07-08 more algebraic properties for gcd/lcm
2015-07-08 haftmann 2015-07-08 moved normalization and unit_factor into Main HOL corpus
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-25 haftmann 2015-06-25 more theorems
2015-06-23 paulson 2015-06-23 Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-06-12 haftmann 2015-06-12 uniform _ div _ as infix syntax for ring division
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-04-12 hoelzl 2015-04-12 move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
2015-04-09 hoelzl 2015-04-09 replace almost_everywhere_zero by Infinite_Set.MOST
2015-03-23 haftmann 2015-03-23 explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2015-02-06 haftmann 2015-02-06 default abstypes and default abstract equations make technical (no_code) annotation superfluous
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-02 haftmann 2014-10-02 formal lcm definition for polynomials
2014-09-07 haftmann 2014-09-07 explicit theory with additional, less commonly used list operations
2014-08-05 wenzelm 2014-08-05 tuned proofs;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-07-01 huffman 2014-07-01 add lemmas: polynomial div/mod distribute over addition
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-03 paulson 2014-04-03 Cleaned up some messy proofs
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
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'