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