| Thu, 30 Mar 2000 19:45:51 +0200 |
nipkow |
recdef.rules -> recdef.simps
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 15:48:13 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:19:38 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Fri, 03 Jul 1998 10:55:32 +0200 |
nipkow |
Removed leading !! in goals
|
file |
diff |
annotate
|
| Mon, 22 Jun 1998 17:26:46 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
| Sat, 07 Mar 1998 16:29:29 +0100 |
nipkow |
Removed `addsplits [expand_if]'
|
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, 03 Nov 1997 09:57:35 +0100 |
nipkow |
expand_option_case -> split_option_case
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 15:25:12 +0200 |
nipkow |
setloop split_tac -> addsplits
|
file |
diff |
annotate
|
| Mon, 29 Sep 1997 11:37:02 +0200 |
paulson |
Step_tac -> Safe_tac
|
file |
diff |
annotate
|
| Tue, 03 Jun 1997 12:03:38 +0200 |
paulson |
No longer refers to internal TFL structures
|
file |
diff |
annotate
|
| Mon, 26 May 1997 12:32:35 +0200 |
paulson |
Simplified proofs using expand_option_case
|
file |
diff |
annotate
|
| Thu, 22 May 1997 15:10:59 +0200 |
paulson |
Now uses type option instead of Fail/Subst
|
file |
diff |
annotate
|
| Wed, 21 May 1997 10:53:02 +0200 |
paulson |
Removed rprod from the WF relation; simplified proofs;
|
file |
diff |
annotate
|
| Tue, 20 May 1997 11:42:59 +0200 |
paulson |
Removal of duplicate code from TFL
|
file |
diff |
annotate
|
| Fri, 16 May 1997 13:02:28 +0200 |
oheimb |
renamed unsafe_addss to addss
|
file |
diff |
annotate
|
| Thu, 15 May 1997 12:40:01 +0200 |
paulson |
New version, modified by Konrad Slind and LCP for TFL
|
file |
diff |
annotate
|