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