src/HOL/Isar_examples/Summation.thy
2005-11-16 wenzelm 2005-11-16 tuned document;
2005-05-02 nipkow 2005-05-02 fixed
2005-03-02 nipkow 2005-03-02 another reorganization of setsums and intervals
2004-07-14 nipkow 2004-07-14 ?
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;
2000-12-14 wenzelm 2000-12-14 use \<Sum> from main HOL;
2000-10-03 wenzelm 2000-10-03 tuned;
2000-09-17 wenzelm 2000-09-17 isar-strip-terminators;
2000-08-19 wenzelm 2000-08-19 tuned;
2000-05-05 wenzelm 2000-05-05 adapted to new arithmetic simprocs;
2000-04-01 wenzelm 2000-04-01 tuned presentation;
2000-03-26 wenzelm 2000-03-26 tuned;
1999-10-30 wenzelm 1999-10-30 improved presentation;
1999-10-28 wenzelm 1999-10-28 improved presentation;
1999-10-14 wenzelm 1999-10-14 improved presentation;
1999-10-08 wenzelm 1999-10-08 improved presentation;
1999-10-06 wenzelm 1999-10-06 improved presentation;
1999-10-06 wenzelm 1999-10-06 improved presentation;
1999-09-04 wenzelm 1999-09-04 replaced ?? by ?;
1999-09-02 wenzelm 1999-09-02 renamed NatSum to Summation;