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