| Fri, 07 Sep 2007 15:35:25 +0200 |
paulson |
allow TVars during type inference
|
file |
diff |
annotate
|
| Thu, 06 Sep 2007 17:03:53 +0200 |
paulson |
Vampire structured proofs. Better parsing; some bug fixes.
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 22:35:34 +0200 |
wenzelm |
replaced ProofContext.infer_types by general Syntax.check_terms;
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:16:44 +0200 |
paulson |
Returning both a "one-line" proof and a structured proof
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 18:30:11 +0200 |
paulson |
Modified message for sendback
|
file |
diff |
annotate
|
| Wed, 08 Aug 2007 13:59:46 +0200 |
paulson |
Fixing the code to undo the function ascii_of
|
file |
diff |
annotate
|
| Tue, 17 Jul 2007 16:06:13 +0200 |
paulson |
Full sort information by default.
|
file |
diff |
annotate
|
| Fri, 29 Jun 2007 18:21:25 +0200 |
paulson |
bug fixes to proof reconstruction
|
file |
diff |
annotate
|
| Thu, 31 May 2007 01:25:24 +0200 |
wenzelm |
TextIO.inputLine: use present SML B library version;
|
file |
diff |
annotate
|
| Wed, 23 May 2007 14:52:12 +0200 |
paulson |
formatting
|
file |
diff |
annotate
|
| Thu, 19 Apr 2007 18:23:11 +0200 |
paulson |
trying to make single-step proofs work better, especially if they contain
|
file |
diff |
annotate
|
| Wed, 18 Apr 2007 21:30:14 +0200 |
wenzelm |
simplified ProofContext.infer_types(_pats);
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:31:49 +0200 |
wenzelm |
proper ProofContext.infer_types;
|
file |
diff |
annotate
|
| Thu, 29 Mar 2007 11:12:03 +0200 |
paulson |
Now checks for types-only clause before outputting.
|
file |
diff |
annotate
|
| Wed, 21 Mar 2007 13:58:36 +0100 |
paulson |
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
|
file |
diff |
annotate
|
| Mon, 19 Mar 2007 15:57:20 +0100 |
paulson |
No label on "show"; tries to remove dependencies more cleanly
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 13:10:22 +0100 |
paulson |
First stab at reconstructing HO problems
|
file |
diff |
annotate
|
| Wed, 28 Feb 2007 12:51:46 +0100 |
paulson |
Now outputs metis calls
|
file |
diff |
annotate
|
| Sat, 20 Jan 2007 14:09:14 +0100 |
wenzelm |
Output.debug: non-strict;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2007 18:12:59 +0100 |
paulson |
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
|
file |
diff |
annotate
|
| Fri, 05 Jan 2007 13:36:32 +0100 |
paulson |
Proof.context now sent to watcher and used in type inference step of proof reconstruction
|
file |
diff |
annotate
|
| Thu, 04 Jan 2007 17:55:12 +0100 |
paulson |
improvements to proof reconstruction. Some files loaded in a different order
|
file |
diff |
annotate
|
| Wed, 03 Jan 2007 18:29:46 +0100 |
paulson |
Improvements to proof reconstruction. Now "fixes" is inserted
|
file |
diff |
annotate
|
| Wed, 03 Jan 2007 11:06:52 +0100 |
paulson |
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
|
file |
diff |
annotate
|