src/HOL/Library/Polynomial_Factorial.thy
2017-01-17 wenzelm 2017-01-17 isabelle update_cartouches -c -t;
2017-01-09 haftmann 2017-01-09 generalized definition
2017-01-09 haftmann 2017-01-09 gcd/lcm on finite sets
2017-01-09 haftmann 2017-01-09 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
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-04 haftmann 2017-01-04 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
2017-01-04 haftmann 2017-01-04 reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
2016-12-17 haftmann 2016-12-17 restructured matter on polynomials and normalized fractions
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-10-16 haftmann 2016-10-16 more standardized theorem names for facts involving the div and mod identity
2016-10-16 haftmann 2016-10-16 more standardized names
2016-10-12 haftmann 2016-10-12 separate type class for arbitrary quotient and remainder partitions
2016-09-29 paulson 2016-09-29 Generalised the type of map_poly
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-16 haftmann 2016-09-16 prefer abbreviation for trivial set conversion
2016-09-09 nipkow 2016-09-09 msetsum -> set_mset, msetprod -> prod_mset
2016-09-01 wenzelm 2016-09-01 tuned headers;
2016-08-25 Manuel Eberl 2016-08-25 Deprivatisation of lemmas in Polynomial_Factorial
2016-08-16 eberlm 2016-08-16 Polynomial algebra cleanup (tuned)
2016-08-16 eberlm 2016-08-16 Polynomial algebra cleanup