src/HOL/ex/NatSum.thy
Sun, 24 Oct 2010 20:19:00 +0200 nipkow nat_number -> eval_nat_numeral
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
Wed, 20 Jun 2007 05:18:39 +0200 huffman 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
Wed, 08 Nov 2006 23:11:13 +0100 wenzelm moved theories Parity, GCD, Binomial to Library;
Thu, 02 Nov 2006 13:35:09 +0100 nipkow added sum_squared
Mon, 01 Aug 2005 19:20:47 +0200 wenzelm tuned;
Tue, 28 Jun 2005 17:56:04 +0200 paulson stylistic improvements
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Wed, 02 Mar 2005 12:06:15 +0100 nipkow another reorganization of setsums and intervals
Thu, 05 Aug 2004 10:51:30 +0200 paulson an updated treatment of the simprules
Thu, 15 Jul 2004 13:11:34 +0200 nipkow Moved to new m<..<n syntax for set intervals.
Thu, 15 Nov 2001 16:12:49 +0100 paulson new theories from Jacques Fleuriot
Sat, 03 Nov 2001 01:33:54 +0100 wenzelm tuned;
Mon, 15 Oct 2001 20:42:06 +0200 wenzelm setsum syntax;
Sat, 06 Oct 2001 00:02:46 +0200 wenzelm * sane numerals (stage 2): plain "num" syntax (removed "#");
Fri, 05 Oct 2001 21:52:39 +0200 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
Thu, 27 Sep 2001 15:42:08 +0200 wenzelm tuned;
Mon, 25 Jun 2001 15:35:59 +0200 paulson Simprocs for type "nat" no longer introduce numerals unless they are already
Thu, 01 Feb 2001 20:51:13 +0100 wenzelm converted to new-style theories;
Wed, 24 May 2000 12:21:26 +0200 paulson restored NatSum.thy
Mon, 08 May 2000 16:59:18 +0200 paulson new example
Wed, 08 Mar 2000 16:24:46 +0100 paulson tidied
Fri, 24 Jul 1998 13:19:38 +0200 berghofe Adapted to new datatype package.
Wed, 21 May 1997 10:55:21 +0200 paulson Function "sum" now defined using primrec
Mon, 05 Feb 1996 21:29:06 +0100 clasohm expanded tabs; incorporated Konrad's changes
Fri, 01 Dec 1995 12:03:13 +0100 clasohm removed quotes from consts and syntax sections
Wed, 22 Mar 1995 12:42:34 +0100 clasohm converted ex with curried function application
less more (0) tip