src/HOL/Computational_Algebra/Polynomial.thy
Mon, 29 Mar 2021 12:26:13 +0100 paulson removal of needless hypothesis in hd_rev and last_rev
Sat, 09 Jan 2021 15:56:09 +0100 Manuel Eberl Corrected lemma that was too specific in HOL-Computational_Algebra
Fri, 08 Jan 2021 19:52:10 +0100 Manuel Eberl some algebra material for HOL: characteristic of a ring, algebraic integers
Fri, 27 Nov 2020 21:19:52 +0000 paulson More removal of apply
Sun, 15 Nov 2020 13:08:13 +0000 paulson trival
Thu, 27 Aug 2020 12:14:46 +0100 paulson tidying up some theorem statements
Sat, 11 Jul 2020 18:09:09 +0000 haftmann a generic horner sum operation
Sun, 22 Mar 2020 19:02:39 +0000 paulson new-style Greater lemmas
Tue, 21 Jan 2020 11:02:27 +0100 Manuel Eberl Removed multiplicativity assumption from normalization_semidom
Wed, 10 Apr 2019 21:29:32 +0100 paulson Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
Wed, 10 Apr 2019 13:34:55 +0100 paulson The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Mon, 24 Sep 2018 14:30:09 +0200 nipkow Prefix form of infix with * on either side no longer needs special treatment
Thu, 20 Sep 2018 18:20:02 +0100 paulson removal of more redundancies, and fixes
Wed, 22 Aug 2018 13:33:50 +0000 haftmann prefer constructive primitive_part over implicit content_decompose
Fri, 29 Jun 2018 14:00:37 +0100 paulson Now based on Complex_Main, not HOL.Deriv
Thu, 28 Jun 2018 17:14:40 +0100 paulson Incorporating new/strengthened proofs from Library and AFP entries
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sun, 07 Jan 2018 22:15:54 +0100 wenzelm prefer formal comments;
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
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
Sun, 08 Oct 2017 22:28:19 +0200 haftmann tuned
Tue, 29 Aug 2017 16:24:14 +0200 eberlm Some small lemmas about polynomials and FPSs
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Thu, 11 May 2017 16:47:53 +0200 haftmann more lemmas
Tue, 25 Apr 2017 08:38:23 +0200 haftmann instance for polynomial rings with characteristic zero
Mon, 17 Apr 2017 16:39:01 +0200 haftmann more systematic treatment of polynomial 1
Sun, 16 Apr 2017 15:30:03 +0200 haftmann more rules concerning of_nat, of_int, numeral
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