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