src/HOL/Binomial.thy
Sat, 02 Jul 2016 08:41:05 +0200 haftmann more correct comment
Thu, 16 Jun 2016 17:57:09 +0200 eberlm Various additions to polynomials, FPSs, Gamma function
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Tue, 01 Mar 2016 10:36:19 +0100 haftmann tuned bootstrap order to provide type classes in a more sensible order
Fri, 19 Feb 2016 13:40:50 +0100 hoelzl generalize more theorems to support enat and ennreal
Wed, 17 Feb 2016 21:51:57 +0100 haftmann generalized some lemmas;
Wed, 17 Feb 2016 21:51:56 +0100 haftmann pulled out legacy aliasses and infamous dvd interpretations into theory appendix
Tue, 12 Jan 2016 16:59:32 +0100 eberlm Deleted problematic code equation in Binomial temporarily.
Mon, 11 Jan 2016 16:38:39 +0100 eberlm Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 23 Nov 2015 16:57:54 +0000 paulson New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
Fri, 13 Nov 2015 12:27:13 +0000 paulson Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
Tue, 03 Nov 2015 15:24:24 +0100 eberlm added acknowledgement in Binomial.thy
Mon, 02 Nov 2015 16:17:09 +0100 eberlm Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
Mon, 02 Nov 2015 11:56:28 +0100 eberlm Rounding function, uniform limits, cotangent, binomial identities
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 16 Jun 2015 11:31:22 +0200 hoelzl tuned src/HOL/ex/Ballot
Mon, 25 May 2015 22:11:43 +0200 wenzelm merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
Sun, 03 May 2015 16:45:07 +0200 wenzelm tuned;
Tue, 21 Apr 2015 17:19:00 +0100 paulson New material, mostly about limits. Consolidation.
Tue, 31 Mar 2015 21:54:32 +0200 haftmann given up separate type classes demanding `inverse 0 = 0`
Tue, 31 Mar 2015 15:00:03 +0100 paulson New material and binomial fix
Tue, 17 Mar 2015 15:11:25 +0000 paulson more general type class for factorial. Now allows code generation (?)
Mon, 16 Mar 2015 15:30:00 +0000 paulson The factorial function, "fact", now has type "nat => 'a"
Tue, 10 Mar 2015 16:12:35 +0000 paulson renaming HOL/Fact.thy -> Binomial.thy
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Fri, 17 Mar 2006 10:04:27 +0100 ballarin Renamed setsum_mult to setsum_right_distrib.
Tue, 20 Sep 2005 14:03:37 +0200 wenzelm tuned theory dependencies;
Thu, 07 Jul 2005 12:36:56 +0200 nipkow Used to be part of Finite_Set (or was it SetInterval?)
less more (0) tip