| 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
|
| 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
|