| Mon, 22 Jan 2001 17:26:19 +0100 | paulson | deleted several obsolete lemmas from NatArith.ML | file | diff | annotate |
| Tue, 19 Dec 2000 15:14:36 +0100 | paulson | cancel-factor simproc allows shorter proofs | file | diff | annotate |
| Mon, 02 Oct 2000 14:32:33 +0200 | nipkow | *** empty log message *** | file | diff | annotate |
| Wed, 19 Jul 2000 18:57:27 +0200 | oheimb | corrected header | file | diff | annotate |
| Mon, 26 Jun 2000 16:18:51 +0200 | oheimb | corrected specifications and simplified proofs | file | diff | annotate |
| Thu, 04 May 2000 15:15:37 +0200 | paulson | changed 2 to #2 | file | diff | annotate |
| Mon, 13 Mar 2000 16:23:34 +0100 | wenzelm | case_tac now subsumes both boolean and datatype cases; | file | diff | annotate |
| Mon, 13 Mar 2000 12:51:10 +0100 | nipkow | exhaust_tac -> cases_tac | file | diff | annotate |
| Mon, 23 Aug 1999 15:30:26 +0200 | wenzelm | isatool expandshort; | file | diff | annotate |
| Thu, 10 Jun 1999 16:46:59 +0200 | nipkow | unclosed comment. | file | diff | annotate |
| Tue, 08 Jun 1999 12:53:20 +0200 | nipkow | added square root example. | file | diff | annotate |
| Fri, 29 Jan 1999 16:26:12 +0100 | paulson | expandshort | file | diff | annotate |
| Fri, 27 Nov 1998 17:00:30 +0100 | nipkow | At last: linear arithmetic for nat! | file | diff | annotate |
| Fri, 16 Oct 1998 17:32:29 +0200 | nipkow | Mods because of: Installed trans_tac in solver of simpset(). | file | diff | annotate |
| Wed, 14 Oct 1998 15:26:31 +0200 | nipkow | New many-sorted version. | file | diff | annotate |
| Thu, 01 Oct 1998 18:23:00 +0200 | paulson | tidied | file | diff | annotate |
| Wed, 19 Aug 1998 10:28:25 +0200 | paulson | Tidied, removing uses of less_imp_diff_positive | file | diff | annotate |
| Fri, 24 Jul 1998 13:03:20 +0200 | berghofe | Adapted to new datatype package. | file | diff | annotate |
| Mon, 22 Jun 1998 17:26:46 +0200 | wenzelm | isatool fixgoal; | file | diff | annotate |
| Mon, 09 Mar 1998 16:17:28 +0100 | wenzelm | eliminated pred function; | file | diff | annotate |
| Thu, 04 Dec 1997 09:05:59 +0100 | nipkow | Simplified proofs. | file | diff | annotate |
| Wed, 03 Dec 1997 17:25:43 +0100 | nipkow | Replaced n ~= 0 by 0 < n | file | diff | annotate |
| Wed, 05 Nov 1997 13:23:46 +0100 | paulson | Ran expandshort, especially to introduce Safe_tac | file | diff | annotate |
| Mon, 03 Nov 1997 12:13:18 +0100 | wenzelm | isatool fixclasimp; | file | diff | annotate |
| Fri, 30 May 1997 15:21:21 +0200 | paulson | Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs | file | diff | annotate |
| Thu, 26 Sep 1996 12:47:47 +0200 | paulson | Ran expandshort | file | diff | annotate |
| Fri, 19 Jul 1996 15:56:01 +0200 | berghofe | Classical tactics now use default claset. | file | diff | annotate |
| Fri, 14 Jun 1996 12:25:02 +0200 | paulson | Explicitly included add_mult_distrib & add_mult_distrib2 | file | diff | annotate |
| Tue, 30 Jan 1996 15:24:36 +0100 | clasohm | expanded tabs | file | diff | annotate |
| Fri, 17 Nov 1995 09:04:10 +0100 | nipkow | New directory. | file | diff | annotate |