src/HOL/Library/Polynomial.thy
Wed, 20 Apr 2016 16:01:59 +0200 wenzelm proper latex;
Fri, 15 Apr 2016 10:19:35 +0200 Rene Thiemann several updates on polynomial long division and pseudo division
Thu, 25 Feb 2016 16:44:53 +0100 eberlm Tuned Euclidean rings
Wed, 17 Feb 2016 21:51:58 +0100 haftmann separated potentially conflicting type class instance into separate theory
Wed, 17 Feb 2016 21:51:58 +0100 haftmann gcd instances for poly
Mon, 11 Jan 2016 16:38:39 +0100 eberlm Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
Tue, 05 Jan 2016 21:57:21 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 05 Jan 2016 20:23:49 +0100 eberlm Fixed sectioning in HOL/Library/Polynomial
Tue, 05 Jan 2016 17:54:10 +0100 eberlm Added some facts about polynomials
Mon, 28 Dec 2015 01:28:28 +0100 wenzelm more symbols;
Mon, 09 Nov 2015 15:48:17 +0100 wenzelm qualifier is mandatory by default;
Thu, 05 Nov 2015 10:39:49 +0100 wenzelm isabelle update_cartouches -c -t;
Thu, 24 Sep 2015 13:33:42 +0200 wenzelm explicit indication of overloaded typedefs;
Wed, 08 Jul 2015 14:01:39 +0200 haftmann more algebraic properties for gcd/lcm
Wed, 08 Jul 2015 14:01:34 +0200 haftmann moved normalization and unit_factor into Main HOL corpus
Mon, 06 Jul 2015 22:57:34 +0200 wenzelm tuned proofs;
Thu, 25 Jun 2015 15:01:42 +0200 haftmann more theorems
Tue, 23 Jun 2015 16:55:28 +0100 paulson 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.
Wed, 17 Jun 2015 11:03:05 +0200 wenzelm isabelle update_cartouches;
Fri, 12 Jun 2015 08:53:23 +0200 haftmann uniform _ div _ as infix syntax for ring division
Mon, 01 Jun 2015 18:59:21 +0200 haftmann separate class for division operator, with particular syntax added in more specific classes
Sun, 12 Apr 2015 11:34:09 +0200 hoelzl move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
Thu, 09 Apr 2015 15:17:21 +0200 hoelzl replace almost_everywhere_zero by Infinite_Set.MOST
Mon, 23 Mar 2015 19:05:14 +0100 haftmann explicit commutative additive inverse operation;
Thu, 19 Feb 2015 11:53:36 +0100 haftmann establish unique preferred fact names
Fri, 06 Feb 2015 17:57:03 +0100 haftmann default abstypes and default abstract equations make technical (no_code) annotation superfluous
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Thu, 02 Oct 2014 11:33:08 +0200 haftmann formal lcm definition for polynomials
Sun, 07 Sep 2014 09:49:05 +0200 haftmann explicit theory with additional, less commonly used list operations
Tue, 05 Aug 2014 12:56:15 +0200 wenzelm tuned proofs;
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Tue, 01 Jul 2014 21:57:08 -0700 huffman add lemmas: polynomial div/mod distribute over addition
Sat, 12 Apr 2014 17:26:27 +0200 nipkow made mult_pos_pos a simp rule
Thu, 03 Apr 2014 17:26:04 +0100 paulson Cleaned up some messy proofs
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
Wed, 12 Feb 2014 08:37:06 +0100 blanchet adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed 'nat_{case,rec}' to '{case,rec}_nat'
Tue, 24 Dec 2013 11:24:14 +0100 haftmann more general induction rule;
Mon, 23 Dec 2013 20:45:33 +0100 haftmann convenient printing of polynomial values
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Sat, 15 Jun 2013 17:19:23 +0200 haftmann lifting for primitive definitions;
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Fri, 06 Apr 2012 12:45:56 +0200 wenzelm fixed document;
Tue, 03 Apr 2012 15:15:00 +0200 huffman modernized obsolete old-style theory name with proper new-style underscore
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Sun, 18 Mar 2012 08:57:45 +0100 haftmann comments for uniformity
Thu, 29 Dec 2011 10:47:56 +0100 haftmann tuned declaration
Tue, 20 Dec 2011 17:40:18 +0100 bulwahn adding quickcheck generators in some HOL-Library theories
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Sun, 20 Nov 2011 21:05:23 +0100 wenzelm eliminated obsolete "standard";
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Mon, 12 Jul 2010 11:39:27 +0200 haftmann avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
Mon, 12 Jul 2010 08:58:13 +0200 haftmann dropped superfluous [code del]s
Mon, 26 Apr 2010 11:34:19 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps
less more (0) -60 tip