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