src/HOL/Computational_Algebra/Polynomial_Factorial.thy
Wed, 22 Aug 2018 13:33:50 +0000 haftmann prefer constructive primitive_part over implicit content_decompose
Sat, 11 Nov 2017 18:41:08 +0000 haftmann dedicated definition for coprimality
Mon, 09 Oct 2017 19:10:52 +0200 haftmann canonical multiplicative euclidean size
Mon, 09 Oct 2017 19:10:49 +0200 haftmann clarified uniqueness criterion for euclidean rings
Sun, 08 Oct 2017 22:28:22 +0200 haftmann euclidean rings need no normalization
Sun, 08 Oct 2017 22:28:21 +0200 haftmann elementary definition of division on natural numbers
Sun, 08 Oct 2017 22:28:21 +0200 haftmann abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
Sun, 08 Oct 2017 22:28:21 +0200 haftmann Polynomial_Factorial does not depend on Field_as_Ring as such
Tue, 30 May 2017 14:04:48 +0200 nipkow tuned names
Tue, 30 May 2017 10:03:35 +0200 nipkow redefined Greatest
Mon, 17 Apr 2017 16:39:01 +0200 haftmann more systematic treatment of polynomial 1
Fri, 07 Apr 2017 21:17:18 +0200 wenzelm tuned headers;
Thu, 06 Apr 2017 21:37:13 +0200 haftmann session containing computational algebra
less more (0) tip