src/HOL/Library/Binomial.thy
2013-08-07 wenzelm 2013-08-07 tuned proofs;
2012-11-27 hoelzl 2012-11-27 add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
2012-11-26 hoelzl 2012-11-26 add binomial_ge_n_over_k_pow_k
2012-08-16 wenzelm 2012-08-16 tuned proofs;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-02 bulwahn 2012-03-02 removing finiteness goals
2012-02-16 wenzelm 2012-02-16 tuned proofs;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-04-23 haftmann 2010-04-23 epheremal replacement of field_simps by field_eq_simps
2010-02-24 haftmann 2010-02-24 renamed theory Rational to Rat
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-07-23 chaieb 2009-07-23 merged
2009-07-23 chaieb 2009-07-23 More theorems about pochhammer
2009-07-15 chaieb 2009-07-15 Moved theorem binomial_symmetric from Formal_Power_Series to here
2009-07-17 avigad 2009-07-17 Changed fact_Suc_nat back to fact_Suc
2009-07-14 avigad 2009-07-14 Repairs regarding new Fact.thy.
2009-05-28 huffman 2009-05-28 use class field_char_0
2009-05-16 nipkow 2009-05-16 "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-01 nipkow 2009-04-01 cleaned up setprod_zero-related lemmas
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-02-16 haftmann 2009-02-16 new primrec
2009-02-15 nipkow 2009-02-15 more finiteness
2009-02-13 huffman 2009-02-13 section -> subsection
2009-01-30 chaieb 2009-01-30 Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2007-12-18 haftmann 2007-12-18 switched from PreList to ATP_Linkup
2007-12-10 haftmann 2007-12-10 switched import from Main to PreList
2007-11-10 wenzelm 2007-11-10 tuned document;
2007-10-23 nipkow 2007-10-23 went back to >0
2007-10-21 nipkow 2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-10-20 chaieb 2007-10-20 fixed proofs
2006-11-09 wenzelm 2006-11-09 tuned;
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;