src/HOL/Number_Theory/Binomial.thy
2014-10-30 paulson 2014-10-30 choose_reduce_nat: re-ordered operands
2014-10-20 paulson 2014-10-20 tweaked
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-09-05 paulson 2014-09-05 Generalised card_length_listsum to all m
2014-09-05 nipkow 2014-09-05 added lemma
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-05-30 hoelzl 2014-05-30 introduce more powerful reindexing rules for big operators
2014-03-17 paulson 2014-03-17 a few new theorems
2014-01-25 wenzelm 2014-01-25 explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
2014-01-24 paulson 2014-01-24 Restored Suc rather than +1, and using Library/Binimial
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-02-27 Andreas Lochbihler 2013-02-27 use lemma from Big_Operators
2013-02-27 Andreas Lochbihler 2013-02-27 add inclusion/exclusion lemma
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2011-12-19 noschinl 2011-12-19 add lemmas
2011-09-10 wenzelm 2011-09-10 misc tuning;
2011-03-13 wenzelm 2011-03-13 tuned headers;
2011-01-13 wenzelm 2011-01-13 eliminated global prems; tuned proofs;
2010-12-21 nipkow 2010-12-21 tuned proof
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-03-11 haftmann 2010-03-11 deleted default simp rule card.insert
2010-03-08 haftmann 2010-03-08 transfer: avoid camel case
2009-09-01 haftmann 2009-09-01 some reorganization of number theory