| Thu, 25 May 2000 15:20:44 +0200 | paulson | setsum replaces sum_below | file | diff | annotate |
| Tue, 23 May 2000 12:35:57 +0200 | paulson | Sums of geometric series | file | diff | annotate |
| Fri, 12 May 2000 15:20:46 +0200 | paulson | new simprules needed because of new subtraction rewriting | file | diff | annotate |
| Tue, 09 May 2000 11:29:13 +0200 | paulson | more examples | file | diff | annotate |
| Mon, 08 May 2000 18:20:04 +0200 | paulson | yet another example | file | diff | annotate |
| Mon, 08 May 2000 16:59:18 +0200 | paulson | new example | file | diff | annotate |
| Tue, 02 May 2000 18:54:59 +0200 | paulson | now using binary naturals | file | diff | annotate |
| Sun, 23 Apr 2000 11:41:45 +0200 | paulson | new, but still slow, proofs using binary numerals | file | diff | annotate |
| Fri, 17 Mar 2000 15:51:13 +0100 | paulson | re-ordered the theorems | file | diff | annotate |
| Fri, 10 Mar 2000 17:53:16 +0100 | paulson | tidied | file | diff | annotate |
| Wed, 08 Mar 2000 16:24:46 +0100 | paulson | tidied | file | diff | annotate |
| Tue, 28 Jul 1998 16:36:32 +0200 | paulson | Tidied | file | diff | annotate |
| Mon, 22 Jun 1998 17:26:46 +0200 | wenzelm | isatool fixgoal; | file | diff | annotate |
| Mon, 12 Jan 1998 17:26:34 +0100 | wenzelm | Delsimprocs nat_cancel; | file | diff | annotate |
| Thu, 20 Nov 1997 11:55:39 +0100 | paulson | Now uses induct_tac | file | diff | annotate |
| Fri, 10 Oct 1997 19:02:28 +0200 | wenzelm | fixed dots; | file | diff | annotate |
| Thu, 21 Aug 1997 12:54:20 +0200 | paulson | Replaced Suc(Suc 0) by 2; it improves readability a little | file | diff | annotate |
| Wed, 21 May 1997 10:55:21 +0200 | paulson | Function "sum" now defined using primrec | file | diff | annotate |
| Fri, 14 Jun 1996 12:37:21 +0200 | paulson | Explicitly included add_mult_distrib & add_mult_distrib2 | file | diff | annotate |
| Mon, 03 Jun 1996 11:41:26 +0200 | paulson | Used 2 instead of Suc(Suc 0) | file | diff | annotate |
| Tue, 30 Jan 1996 15:24:36 +0100 | clasohm | expanded tabs | file | diff | annotate |
| Wed, 04 Oct 1995 13:12:14 +0100 | clasohm | added local simpsets | file | diff | annotate |
| Wed, 22 Mar 1995 12:42:34 +0100 | clasohm | converted ex with curried function application | file | diff | annotate |