| Thu, 20 Dec 2007 11:16:19 +0100 |
wenzelm |
made refute non-critical (seems to work after avoiding floating point random numbers);
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 23:06:13 +0100 |
wenzelm |
removed duplicate CRITICAL markup;
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 17:40:48 +0100 |
paulson |
Replaced refs by config params; finer critical section in mets method
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 16:52:07 +0100 |
wenzelm |
marked refute (the main metis procedure) as CRITICAL;
|
file |
diff |
annotate
|
| Tue, 18 Dec 2007 17:37:25 +0100 |
paulson |
Deleted redundant setmp calls
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 16:51:39 +0200 |
paulson |
reconstruction bug fix
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 15:59:31 +0200 |
paulson |
rationalized redundant code
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 10:50:11 +0200 |
paulson |
getting rid of type typ_var
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 18:14:00 +0200 |
paulson |
context-based treatment of generalization; also handling TFrees in axiom clauses
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2007 09:59:21 +0200 |
paulson |
metis method: used theorems
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 12:32:58 +0200 |
paulson |
combinator translation
|
file |
diff |
annotate
|
| Fri, 31 Aug 2007 18:46:34 +0200 |
wenzelm |
type_infer: mode_pattern;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 22:35:38 +0200 |
wenzelm |
replaced ProofContext.infer_types by general Syntax.check_terms;
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:15:58 +0200 |
paulson |
Reconstruction bug fix
|
file |
diff |
annotate
|
| Sat, 18 Aug 2007 13:32:20 +0200 |
wenzelm |
export more tactics;
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 23:10:39 +0200 |
wenzelm |
turned type_lits into configuration option (with attribute);
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 00:03:50 +0200 |
wenzelm |
proper signature for Meson;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:29:57 +0200 |
wenzelm |
metis_tac: proper context (ProofContext.init it *not* sufficient);
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 23:19:18 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 22:07:52 +0200 |
wenzelm |
The Metis prover (slightly modified version from Larry);
|
file |
diff |
annotate
|