src/HOL/Binomial.thy
2017-04-22 wenzelm 2017-04-22 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
2017-04-03 eberlm 2017-04-03 added shuffle product to HOL/List
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-10-16 haftmann 2016-10-16 more standardized names
2016-09-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-09-15 nipkow 2016-09-15 renamed listsum -> sum_list, listprod ~> prod_list
2016-08-26 Manuel Eberl 2016-08-26 Bohr-Mollerup theorem for the Gamma function
2016-08-12 wenzelm 2016-08-12 more symbols;
2016-08-10 nipkow 2016-08-10 "split add" -> "split"
2016-07-20 wenzelm 2016-07-20 unused (see also 651ea265d568);
2016-07-12 wenzelm 2016-07-12 misc tuning and modernization;
2016-07-09 haftmann 2016-07-09 more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat * * * more rules for setsum, setprod on intervals
2016-07-04 haftmann 2016-07-04 tuned sections
2016-07-04 haftmann 2016-07-04 relating gbinomial and binomial, still using distinct definitions
2016-07-02 haftmann 2016-07-02 simplified definitions of combinatorial functions
2016-07-02 haftmann 2016-07-02 define binomial coefficents directly via combinatorial definition
2016-07-02 haftmann 2016-07-02 more correct comment
2016-06-16 eberlm 2016-06-16 Various additions to polynomials, FPSs, Gamma function
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-01 haftmann 2016-03-01 tuned bootstrap order to provide type classes in a more sensible order
2016-02-19 hoelzl 2016-02-19 generalize more theorems to support enat and ennreal
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2016-02-17 haftmann 2016-02-17 pulled out legacy aliasses and infamous dvd interpretations into theory appendix
2016-01-12 eberlm 2016-01-12 Deleted problematic code equation in Binomial temporarily.
2016-01-11 eberlm 2016-01-11 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-23 paulson 2015-11-23 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-03 eberlm 2015-11-03 added acknowledgement in Binomial.thy
2015-11-02 eberlm 2015-11-02 Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
2015-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-16 hoelzl 2015-06-16 tuned src/HOL/ex/Ballot
2015-05-25 wenzelm 2015-05-25 merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
2015-05-03 wenzelm 2015-05-03 tuned;
2015-04-21 paulson 2015-04-21 New material, mostly about limits. Consolidation.
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-31 paulson 2015-03-31 New material and binomial fix
2015-03-17 paulson 2015-03-17 more general type class for factorial. Now allows code generation (?)
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2015-03-10 paulson 2015-03-10 renaming HOL/Fact.thy -> Binomial.thy
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-03-17 ballarin 2006-03-17 Renamed setsum_mult to setsum_right_distrib.
2005-09-20 wenzelm 2005-09-20 tuned theory dependencies;
2005-07-07 nipkow 2005-07-07 Used to be part of Finite_Set (or was it SetInterval?) Added binomial thm.