src/HOL/ex/NatSum.ML
Mon, 12 Jan 1998 17:26:34 +0100 wenzelm Delsimprocs nat_cancel;
Thu, 20 Nov 1997 11:55:39 +0100 paulson Now uses induct_tac
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Thu, 21 Aug 1997 12:54:20 +0200 paulson Replaced Suc(Suc 0) by 2; it improves readability a little
Wed, 21 May 1997 10:55:21 +0200 paulson Function "sum" now defined using primrec
Fri, 14 Jun 1996 12:37:21 +0200 paulson Explicitly included add_mult_distrib & add_mult_distrib2
Mon, 03 Jun 1996 11:41:26 +0200 paulson Used 2 instead of Suc(Suc 0)
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
Wed, 04 Oct 1995 13:12:14 +0100 clasohm added local simpsets
Wed, 22 Mar 1995 12:42:34 +0100 clasohm converted ex with curried function application
less more (0) tip