src/HOL/Library/Polynomial.thy
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'
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2013-12-24 haftmann 2013-12-24 more general induction rule; tuned proofs
2013-12-23 haftmann 2013-12-23 convenient printing of polynomial values
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-06-15 haftmann 2013-06-15 lifting for primitive definitions; explicit conversions from and to lists of coefficients, used for generated code; replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions; prefer pre-existing gcd operation for gcd
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-04-06 wenzelm 2012-04-06 fixed document;
2012-04-03 huffman 2012-04-03 modernized obsolete old-style theory name with proper new-style underscore
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-18 haftmann 2012-03-18 comments for uniformity
2011-12-29 haftmann 2011-12-29 tuned declaration
2011-12-20 bulwahn 2011-12-20 adding quickcheck generators in some HOL-Library theories
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-03-13 wenzelm 2011-03-13 tuned headers;
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-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-07-12 haftmann 2010-07-12 avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
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
2010-01-28 haftmann 2010-01-28 dropped mk_left_commute; use interpretation of locale abel_semigroup instead
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-16 huffman 2009-06-16 smult_dvd lemmas; polynomial gcd
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-22 haftmann 2009-04-22 power operation defined generic
2009-04-16 haftmann 2009-04-16 tightended specification of class semiring_div
2009-03-27 haftmann 2009-03-27 normalized imports
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-02-27 huffman 2009-02-27 make list-style polynomial syntax work when show_sorts is on
2009-02-23 huffman 2009-02-23 add lemmas poly_{div,mod}_minus_{left,right}
2009-02-18 huffman 2009-02-18 move Polynomial.thy to Library