src/HOL/ex/NatSum.thy
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