src/HOL/Library/Polynomial.thy
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
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Thu, 28 Jan 2010 11:48:43 +0100 haftmann dropped mk_left_commute; use interpretation of locale abel_semigroup instead
Sun, 10 Jan 2010 18:43:45 +0100 berghofe Adapted to changes in induct method.
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Tue, 16 Jun 2009 00:01:32 -0700 huffman smult_dvd lemmas; polynomial gcd
Wed, 29 Apr 2009 14:20:26 +0200 haftmann farewell to class recpower
Wed, 22 Apr 2009 19:09:21 +0200 haftmann power operation defined generic
Thu, 16 Apr 2009 10:11:34 +0200 haftmann tightended specification of class semiring_div
Fri, 27 Mar 2009 10:05:11 +0100 haftmann normalized imports
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Fri, 27 Feb 2009 15:37:56 -0800 huffman make list-style polynomial syntax work when show_sorts is on
Mon, 23 Feb 2009 07:19:53 -0800 huffman add lemmas poly_{div,mod}_minus_{left,right}
Wed, 18 Feb 2009 20:14:45 -0800 huffman move Polynomial.thy to Library
less more (0) tip