src/HOL/Binomial.thy
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.