src/HOL/ex/NatSum.thy
2010-10-24 nipkow 2010-10-24 nat_number -> eval_nat_numeral
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-20 huffman 2007-06-20 change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-11-02 nipkow 2006-11-02 added sum_squared
2005-08-01 wenzelm 2005-08-01 tuned;
2005-06-28 paulson 2005-06-28 stylistic improvements
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-03-02 nipkow 2005-03-02 another reorganization of setsums and intervals
2004-08-05 paulson 2004-08-05 an updated treatment of the simprules
2004-07-15 nipkow 2004-07-15 Moved to new m<..<n syntax for set intervals.
2001-11-15 paulson 2001-11-15 new theories from Jacques Fleuriot
2001-11-03 wenzelm 2001-11-03 tuned;
2001-10-15 wenzelm 2001-10-15 setsum syntax;
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-09-27 wenzelm 2001-09-27 tuned;
2001-06-25 paulson 2001-06-25 Simprocs for type "nat" no longer introduce numerals unless they are already present in the expression, and in a coefficient position (i.e. as a factor of a monomial).
2001-02-01 wenzelm 2001-02-01 converted to new-style theories;
2000-05-24 paulson 2000-05-24 restored NatSum.thy
2000-05-08 paulson 2000-05-08 new example
2000-03-08 paulson 2000-03-08 tidied
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1997-05-21 paulson 1997-05-21 Function "sum" now defined using primrec
1996-02-05 clasohm 1996-02-05 expanded tabs; incorporated Konrad's changes
1995-12-01 clasohm 1995-12-01 removed quotes from consts and syntax sections
1995-03-22 clasohm 1995-03-22 converted ex with curried function application