Tue, 16 May 2000 14:07:49 +0200 |
paulson |
changed to cope with the rewriting of #2+n to Suc(Suc n)
|
file |
diff |
annotate
|
Thu, 04 May 2000 15:17:41 +0200 |
paulson |
from Suc...Suc to #m
|
file |
diff |
annotate
|
Tue, 02 May 2000 18:55:11 +0200 |
paulson |
modified for new simprocs
|
file |
diff |
annotate
|
Thu, 30 Mar 2000 19:45:51 +0200 |
nipkow |
recdef.rules -> recdef.simps
|
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
|
Fri, 27 Nov 1998 17:00:30 +0100 |
nipkow |
At last: linear arithmetic for nat!
|
file |
diff |
annotate
|
Thu, 01 Oct 1998 18:29:38 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
Thu, 10 Sep 1998 17:32:07 +0200 |
paulson |
a step to help a proof
|
file |
diff |
annotate
|
Wed, 15 Jul 1998 14:19:02 +0200 |
paulson |
More tidying and removal of "\!\!... from Goal commands
|
file |
diff |
annotate
|
Wed, 15 Jul 1998 10:15:13 +0200 |
paulson |
Removal of leading "\!\!..." from most Goal commands
|
file |
diff |
annotate
|
Thu, 25 Jun 1998 13:57:34 +0200 |
paulson |
Installation of target HOL-Real
|
file |
diff |
annotate
|
Mon, 22 Jun 1998 17:26:46 +0200 |
wenzelm |
isatool fixgoal;
|
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
|
Mon, 23 Jun 1997 10:42:03 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
Mon, 26 May 1997 12:33:03 +0200 |
paulson |
New example ported from ZF
|
file |
diff |
annotate
|