| Sat, 10 Jul 1999 21:48:27 +0200 | wenzelm | handle THM/TERM exn; | file | diff | annotate |
| Thu, 01 Jul 1999 10:32:57 +0200 | paulson | new laws mult_le_cancel1, mult_le_cancel2 | file | diff | annotate |
| Wed, 17 Mar 1999 16:53:46 +0100 | wenzelm | Theory.sign_of; | file | diff | annotate |
| Wed, 03 Mar 1999 11:15:18 +0100 | paulson | expandshort | file | diff | annotate |
| Wed, 27 Jan 1999 17:11:39 +0100 | nipkow | arith_tac for min/max | file | diff | annotate |
| Sun, 24 Jan 1999 11:33:54 +0100 | nipkow | Fixed a bug in lin.arith. | file | diff | annotate |
| Thu, 14 Jan 1999 13:18:09 +0100 | nipkow | More arith refinements. | file | diff | annotate |
| Wed, 13 Jan 1999 12:16:34 +0100 | nipkow | Refined arithmetic. | file | diff | annotate |
| Wed, 13 Jan 1999 08:41:28 +0100 | nipkow | Simplified arithmetic. | file | diff | annotate |
| Tue, 12 Jan 1999 15:59:35 +0100 | nipkow | Restructured Arithmatic | file | diff | annotate |
| Mon, 11 Jan 1999 16:50:49 +0100 | nipkow | More arith simplifications. | file | diff | annotate |
| Sat, 09 Jan 1999 17:55:54 +0100 | nipkow | Remoaved a few now redundant rewrite rules. | file | diff | annotate |
| Sat, 09 Jan 1999 15:24:11 +0100 | nipkow | Refined arith tactic. | file | diff | annotate |
| Tue, 05 Jan 1999 17:27:59 +0100 | nipkow | In Main: moved Bin to the left to preserve the solver in its simpset. | file | diff | annotate |
| Mon, 04 Jan 1999 15:07:47 +0100 | nipkow | Version 1.0 of linear nat arithmetic. | 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 |
| Fri, 23 Oct 1998 20:44:34 +0200 | oheimb | corrected auto_tac (applications of unsafe wrappers) | file | diff | annotate |
| Fri, 16 Oct 1998 17:32:06 +0200 | nipkow | Installed trans_tac in solver of simpset(). | file | diff | annotate |
| Fri, 02 Oct 1998 10:41:35 +0200 | paulson | tidying | file | diff | annotate |
| Thu, 01 Oct 1998 18:29:25 +0200 | nipkow | a few new lemmas. | file | diff | annotate |
| Wed, 23 Sep 1998 10:12:01 +0200 | paulson | deleted needless parentheses | file | diff | annotate |
| Fri, 18 Sep 1998 14:36:03 +0200 | paulson | theorem le_diff_conv2; tidying and expandshort | file | diff | annotate |
| Mon, 14 Sep 1998 10:17:19 +0200 | paulson | new theorem le_diff_conv | file | diff | annotate |
| Mon, 07 Sep 1998 10:40:17 +0200 | paulson | tidying | file | diff | annotate |
| Fri, 04 Sep 1998 11:01:59 +0200 | nipkow | Arith: less_diff_conv | file | diff | annotate |
| Tue, 01 Sep 1998 15:03:10 +0200 | paulson | changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m) | file | diff | annotate |
| Tue, 01 Sep 1998 10:09:11 +0200 | paulson | Two new subtraction lemmas | file | diff | annotate |
| Thu, 20 Aug 1998 16:58:28 +0200 | paulson | new theorems | file | diff | annotate |
| Wed, 19 Aug 1998 10:26:02 +0200 | paulson | Some new theorems. zero_less_diff replaces less_imp_diff_positive | file | diff | annotate |