| Tue, 08 Jun 1999 10:25:12 +0200 |
paulson |
new classical example from Lewis Carroll via S G Pulman
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 15:48:13 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Thu, 16 Jul 1998 10:35:31 +0200 |
paulson |
Addition of "Theorem B" of Peter Andrews
|
file |
diff |
annotate
|
| Mon, 22 Dec 1997 12:21:37 +0100 |
paulson |
New example
|
file |
diff |
annotate
|
| Wed, 03 Dec 1997 11:00:24 +0100 |
paulson |
updated for latest Blast_tac, which treats equality differently
|
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
|
| Sat, 01 Nov 1997 13:00:31 +0100 |
paulson |
mended type constraint\!
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Mon, 26 May 1997 12:53:45 +0200 |
paulson |
Added a missing "result();" after problem 43.
|
file |
diff |
annotate
|
| Wed, 23 Apr 1997 11:05:18 +0200 |
paulson |
Improved indentation of #34
|
file |
diff |
annotate
|
| Mon, 21 Apr 1997 10:14:31 +0200 |
paulson |
Without the type constraint, the inner equality was NOT a biconditional...
|
file |
diff |
annotate
|
| Wed, 09 Apr 1997 12:32:04 +0200 |
paulson |
Using Blast_tac
|
file |
diff |
annotate
|
| Fri, 04 Apr 1997 11:18:52 +0200 |
paulson |
Calls Blast_tac
|
file |
diff |
annotate
|
| Tue, 04 Mar 1997 10:21:16 +0100 |
paulson |
Updated reference to Pelletier erratum
|
file |
diff |
annotate
|
| Fri, 31 Jan 1997 17:50:47 +0100 |
paulson |
Correction to Problem 24
|
file |
diff |
annotate
|
| Mon, 19 Aug 1996 11:19:16 +0200 |
paulson |
Now starts with set_current_thy
|
file |
diff |
annotate
|
| Tue, 30 Jul 1996 18:03:11 +0200 |
berghofe |
Now also Deepen_tac and Best_tac are used.
|
file |
diff |
annotate
|
| Fri, 21 Jun 1996 12:18:50 +0200 |
berghofe |
Classical tactics now use default claset.
|
file |
diff |
annotate
|
| Tue, 28 May 1996 11:16:38 +0200 |
paulson |
Corrected a comment in #34
|
file |
diff |
annotate
|
| Thu, 02 May 1996 12:00:37 +0200 |
paulson |
Restored a proof of Pelletier #38 -- mysteriously deleted
|
file |
diff |
annotate
|
| Wed, 01 May 1996 13:47:21 +0200 |
paulson |
Two new "obvious" examples
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Thu, 14 Dec 1995 12:49:32 +0100 |
paulson |
Added Pelletier's problem 62, as corrected in AAR
|
file |
diff |
annotate
|
| Wed, 22 Mar 1995 12:42:34 +0100 |
clasohm |
converted ex with curried function application
|
file |
diff |
annotate
|