src/HOL/Computational_Algebra/Polynomial_Factorial.thy
23 months ago haftmann 2017-10-09 canonical multiplicative euclidean size
23 months ago haftmann 2017-10-09 clarified uniqueness criterion for euclidean rings
23 months ago haftmann 2017-10-08 euclidean rings need no normalization
23 months ago haftmann 2017-10-08 elementary definition of division on natural numbers
23 months ago haftmann 2017-10-08 abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
23 months ago haftmann 2017-10-08 Polynomial_Factorial does not depend on Field_as_Ring as such
2017-05-30 nipkow 2017-05-30 tuned names
2017-05-30 nipkow 2017-05-30 redefined Greatest
2017-04-17 haftmann 2017-04-17 more systematic treatment of polynomial 1
2017-04-07 wenzelm 2017-04-07 tuned headers;
2017-04-06 haftmann 2017-04-06 session containing computational algebra