Mon, 07 Apr 2008 15:37:04 +0200 |
paulson |
Superficial changes
|
file |
diff |
annotate
|
Thu, 27 Mar 2008 14:41:07 +0100 |
wenzelm |
removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
|
file |
diff |
annotate
|
Wed, 02 Jan 2008 12:22:38 +0100 |
paulson |
testing for empty sort
|
file |
diff |
annotate
|
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
|