| Tue, 08 Jun 1999 10:25:12 +0200 |
paulson |
new classical example from Lewis Carroll via S G Pulman
|
file |
diff |
annotate
|
| Mon, 17 May 1999 10:37:07 +0200 |
paulson |
indentation
|
file |
diff |
annotate
|
| Thu, 22 Oct 1998 10:58:18 +0200 |
paulson |
tidying
|
file |
diff |
annotate
|
| Thu, 16 Jul 1998 10:35:31 +0200 |
paulson |
Addition of "Theorem B" of Peter Andrews
|
file |
diff |
annotate
|
| Tue, 23 Dec 1997 11:37:48 +0100 |
paulson |
New "obvious theorems"
|
file |
diff |
annotate
|
| Wed, 03 Dec 1997 10:47:13 +0100 |
paulson |
updated for latest Blast_tac, which fixes an equality bug
|
file |
diff |
annotate
|
| Mon, 01 Dec 1997 12:50:04 +0100 |
paulson |
speed-up
|
file |
diff |
annotate
|
| Wed, 26 Nov 1997 17:35:08 +0100 |
paulson |
Blast_tac can prove Pelletier\'s problem 46\!
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:24:13 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 15:52:12 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Mon, 29 Sep 1997 11:31:56 +0200 |
paulson |
Step_tac -> Safe_tac
|
file |
diff |
annotate
|
| Wed, 23 Apr 1997 11:00:48 +0200 |
paulson |
Fixed typos in comment
|
file |
diff |
annotate
|
| Wed, 09 Apr 1997 12:34:28 +0200 |
paulson |
Explicit depth bounds seem necessary
|
file |
diff |
annotate
|
| Fri, 04 Apr 1997 11:16:44 +0200 |
paulson |
Now calls Blast_tac and has some hard examples (Halting Problem
|
file |
diff |
annotate
|
| Wed, 05 Mar 1997 10:19:42 +0100 |
paulson |
Added comment
|
file |
diff |
annotate
|
| Tue, 04 Mar 1997 10:21:16 +0100 |
paulson |
Updated reference to Pelletier erratum
|
file |
diff |
annotate
|
| Fri, 14 Feb 1997 10:36:33 +0100 |
paulson |
Added a new challenge problem
|
file |
diff |
annotate
|
| Mon, 10 Feb 1997 12:31:54 +0100 |
paulson |
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
|
file |
diff |
annotate
|
| Fri, 31 Jan 1997 17:17:10 +0100 |
paulson |
Correction to Problem 24
|
file |
diff |
annotate
|
| Fri, 03 Jan 1997 15:01:55 +0100 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
| Mon, 19 Aug 1996 11:22:16 +0200 |
paulson |
Improved the proof of Problem 38
|
file |
diff |
annotate
|
| Mon, 17 Jun 1996 16:51:47 +0200 |
paulson |
Inserted comment about problem 43
|
file |
diff |
annotate
|
| Thu, 04 Apr 1996 18:18:08 +0200 |
paulson |
deleted obsolete comment
|
file |
diff |
annotate
|
| Mon, 11 Mar 1996 14:03:30 +0100 |
paulson |
Added formulation of Halting Problem
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 13:56:16 +0100 |
clasohm |
fixed typo
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:58:15 +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
|
| Thu, 24 Nov 1994 00:31:08 +0100 |
lcp |
updated for new deepen_tac
|
file |
diff |
annotate
|
| Mon, 31 Oct 1994 16:45:19 +0100 |
lcp |
FOL/ex/cla: proofs now use deepen_tac instead of best_tac FOL_dup_cs
|
file |
diff |
annotate
|
| Wed, 19 Oct 1994 09:41:48 +0100 |
lcp |
FOL/ex/cla/58: slightly shorter proof
|
file |
diff |
annotate
|
| Wed, 27 Jul 1994 19:08:14 +0200 |
lcp |
added a new example due to Robin Arthan
|
file |
diff |
annotate
|
| Fri, 17 Jun 1994 17:47:42 +0200 |
lcp |
problem 38 is provable
|
file |
diff |
annotate
|
| Thu, 07 Oct 1993 09:49:46 +0100 |
lcp |
examples now use ~= for "not equals"
|
file |
diff |
annotate
|
| Fri, 24 Sep 1993 11:27:15 +0200 |
lcp |
Added example from Avron: Gentzen-Type Systems, Resolution and Tableaux, JAR 10
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|