| Sun, 14 Oct 2001 20:02:59 +0200 | wenzelm | improved atomize setup; | file | diff | annotate |
| Sat, 06 Oct 2001 00:02:46 +0200 | wenzelm | * sane numerals (stage 2): plain "num" syntax (removed "#"); | file | diff | annotate |
| Fri, 05 Oct 2001 21:52:39 +0200 | wenzelm | sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, | file | diff | annotate |
| Mon, 06 Aug 2001 13:43:24 +0200 | nipkow | turned translation for 1::nat into def. | file | diff | annotate |
| Thu, 31 May 2001 16:07:35 +0200 | nipkow | Allow Suc-numerals as coefficients in lin-arith formulae | file | diff | annotate |
| Tue, 16 Jan 2001 00:28:50 +0100 | wenzelm | tuned atomize; | file | diff | annotate |
| Wed, 03 Jan 2001 11:14:48 +0100 | paulson | removal of the nat_cancel_factor simproc | file | diff | annotate |
| Thu, 21 Dec 2000 16:19:39 +0100 | nipkow | rational arithmetic | file | diff | annotate |
| Mon, 18 Dec 2000 14:59:05 +0100 | nipkow | moved mk_bin from Numerals to HOLogic | file | diff | annotate |
| Fri, 01 Dec 2000 19:53:29 +0100 | nipkow | Linear arithmetic now copes with mixed nat/int formulae. | file | diff | annotate |
| Thu, 23 Nov 2000 21:33:14 +0100 | wenzelm | arith_tac: atomize; | file | diff | annotate |
| Thu, 07 Sep 2000 20:51:07 +0200 | wenzelm | tuned msg; | file | diff | annotate |
| Mon, 14 Aug 2000 14:57:29 +0200 | wenzelm | tuned names; | file | diff | annotate |
| Tue, 25 Jul 2000 00:06:46 +0200 | wenzelm | rearranged setup of arithmetic procedures, avoiding global reference values; | file | diff | annotate |
| Fri, 27 Nov 1998 17:00:30 +0100 | nipkow | At last: linear arithmetic for nat! | file | diff | annotate |
| Wed, 28 Oct 1998 11:25:38 +0100 | nipkow | added nat_diff_split and a few lemmas in Trancl. | file | diff | annotate |
| Thu, 01 Oct 1998 18:23:00 +0200 | paulson | tidied | file | diff | annotate |
| Thu, 24 Sep 1998 17:17:14 +0200 | oheimb | renamed mk_meta_eq to mk_eq | file | diff | annotate |
| Mon, 07 Sep 1998 10:40:17 +0200 | paulson | tidying | file | diff | annotate |
| Tue, 01 Sep 1998 15:05:36 +0200 | paulson | Replaced Suc_diff_n by Suc_diff_le | file | diff | annotate |
| Thu, 20 Aug 1998 16:44:05 +0200 | paulson | adjusted for new rewrites | file | diff | annotate |
| Thu, 13 Aug 1998 18:14:26 +0200 | paulson | even more tidying of Goal commands | file | diff | annotate |
| Wed, 12 Aug 1998 16:20:49 +0200 | oheimb | renamed mk_meta_eq to meta_eq | file | diff | annotate |
| Sun, 12 Jul 1998 11:49:17 +0200 | wenzelm | isatool expandshort; | file | diff | annotate |
| Tue, 03 Mar 1998 15:13:24 +0100 | paulson | New theorem | file | diff | annotate |
| Fri, 05 Dec 1997 17:13:46 +0100 | wenzelm | simplification procedures nat_cancel enabled by default; | file | diff | annotate |
| Mon, 01 Dec 1997 18:27:43 +0100 | wenzelm | open; | file | diff | annotate |
| Mon, 01 Dec 1997 14:42:30 +0100 | berghofe | Added DiffCancelSums. | file | diff | annotate |
| Thu, 27 Nov 1997 13:38:06 +0100 | wenzelm | mk_norm_sum; | file | diff | annotate |
| Wed, 26 Nov 1997 17:52:53 +0100 | wenzelm | separate lists of simprocs; | file | diff | annotate |
| Wed, 26 Nov 1997 16:44:25 +0100 | wenzelm | Setup various arithmetic proof procedures. | file | diff | annotate |