| Fri, 14 Feb 2014 07:53:45 +0100 |
blanchet |
merged 'List.map' and 'List.list.map'
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 13:59:07 +0200 |
blanchet |
minor tweak to error message
|
file |
diff |
annotate
|
| Sat, 11 May 2013 16:13:08 +0200 |
wenzelm |
avoid PolyML.makestring, even in dead code;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2013 17:28:55 +0100 |
blanchet |
use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 17:56:35 +0200 |
blanchet |
never use MaSh in Metis examples, to avoid one dimension of nondeterminism
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:18:55 +0200 |
blanchet |
reintroduced "t@" encoding, this time sound
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
added "args_query" encodings
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
removed killed encodings from Metis examples
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 13:53:09 +0100 |
blanchet |
take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 15:54:51 +0100 |
blanchet |
use SPASS instead of E for Metis examples -- it's seems faster for these small problems
|
file |
diff |
annotate
|
| Mon, 06 Feb 2012 23:01:02 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
example tuning
|
file |
diff |
annotate
|
| Wed, 21 Dec 2011 18:23:08 +0100 |
blanchet |
removed killed encoding from example
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 13:34:12 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 17:26:42 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 12:39:29 +0100 |
huffman |
avoid theorem references like 'semiring_norm(111)'
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
added new tagged encodings to Metis tests
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
added new guards encoding to test
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
rationalize uniform encodings
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 14:43:20 +0200 |
blanchet |
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 16:23:25 +0200 |
blanchet |
"simple" was renamed "mono_simple" and there's now "poly_simple" as well -- but they are not needed here since for Metis they amount to the same as guards
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
rationalized option names -- mono becomes raw_mono and mangled becomes mono
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
include all encodings in tests, now that the incompleteness of some encodings has been addressed
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
made reconstruction of type tag equalities "\?x = \?x" reliable
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
clearer terminology
|
file |
diff |
annotate
|
| Tue, 26 Jul 2011 22:53:06 +0200 |
blanchet |
renamed "preds" encodings to "guards"
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:53:38 +0200 |
blanchet |
test a few more type encodings
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:53:38 +0200 |
blanchet |
renamed "type_sys" to "type_enc", which is more accurate
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
Metis code cleanup
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
more preparations towards hijacking Metis
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
tuned Metis examples
|
file |
diff |
annotate
| base
|