src/HOL/ex/NatSum.thy
2005-08-01 wenzelm tuned;
2005-06-28 paulson stylistic improvements
2005-06-17 haftmann migrated theory headers to new format
2005-03-02 nipkow another reorganization of setsums and intervals
2004-08-05 paulson an updated treatment of the simprules
2004-07-15 nipkow Moved to new m<..<n syntax for set intervals.
2001-11-15 paulson new theories from Jacques Fleuriot
2001-11-03 wenzelm tuned;
2001-10-15 wenzelm setsum syntax;
2001-10-05 wenzelm * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
2001-09-27 wenzelm tuned;
2001-06-25 paulson Simprocs for type "nat" no longer introduce numerals unless they are already
2001-02-01 wenzelm converted to new-style theories;
2000-05-24 paulson restored NatSum.thy
2000-05-08 paulson new example
2000-03-08 paulson tidied
1998-07-24 berghofe Adapted to new datatype package.
1997-05-21 paulson Function "sum" now defined using primrec
1996-02-05 clasohm expanded tabs; incorporated Konrad's changes
1995-12-01 clasohm removed quotes from consts and syntax sections
1995-03-22 clasohm converted ex with curried function application
less more (0) tip