src/HOL/Binomial.thy
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Sun, 16 Oct 2016 09:31:04 +0200 haftmann more standardized names
Mon, 19 Sep 2016 20:06:21 +0200 fleury left_distrib ~> distrib_right, right_distrib ~> distrib_left
Thu, 15 Sep 2016 11:48:20 +0200 nipkow renamed listsum -> sum_list, listprod ~> prod_list
Fri, 26 Aug 2016 11:58:19 +0200 Manuel Eberl Bohr-Mollerup theorem for the Gamma function
Fri, 12 Aug 2016 17:53:55 +0200 wenzelm more symbols;
Wed, 10 Aug 2016 09:33:54 +0200 nipkow "split add" -> "split"
Wed, 20 Jul 2016 11:11:07 +0200 wenzelm unused (see also 651ea265d568);
Tue, 12 Jul 2016 21:53:56 +0200 wenzelm misc tuning and modernization;
Sat, 09 Jul 2016 13:26:16 +0200 haftmann more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
Mon, 04 Jul 2016 19:46:19 +0200 haftmann tuned sections
Mon, 04 Jul 2016 19:46:19 +0200 haftmann relating gbinomial and binomial, still using distinct definitions
Sat, 02 Jul 2016 20:22:25 +0200 haftmann simplified definitions of combinatorial functions
Sat, 02 Jul 2016 15:02:24 +0200 haftmann define binomial coefficents directly via combinatorial definition
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
less more (0) -30 tip