| Tue, 20 Mar 2012 13:53:09 +0100 |
blanchet |
enable "metis_advisory_simp" by default
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 10:06:35 +0100 |
blanchet |
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 12:43:46 +0100 |
blanchet |
better defaults for Metis, that seem to make it less likely to loop seemingly forever -- 0 coefficients might very well make it incomplete
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 16:40:06 +0100 |
wenzelm |
prefer abs_def over def_raw;
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
rename lambda translation schemes
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
|
| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
renamed "sound" option to "strict"
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 23:08:03 +0100 |
blanchet |
killed dead code
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 14:47:08 +0100 |
blanchet |
more robust options
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
wrap lambdas earlier, to get more control over beta/eta
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
move eta-contraction to before translation to Metis, to ensure everything stays in sync
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
avoid that var names get changed by resolution in Metis lambda-lifting
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
avoid spurious messages in "lam_lifting" mode
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
eta-contract to avoid needless "lambda" wrappers
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 17:06:14 +0100 |
blanchet |
give each time slice its own lambda translation
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 13:22:36 +0100 |
blanchet |
make metis reconstruction handling more flexible
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 09:42:27 +0100 |
blanchet |
parse lambda translation option in Metis
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:20:58 +0100 |
blanchet |
rename the lambda translation schemes, so that they are understandable out of context
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:15:51 +0100 |
blanchet |
rename configuration option to more reasonable length
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
continued implementation of lambda-lifting in Metis
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
started implementing lambda-lifting in Metis
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 16:30:47 +0200 |
blanchet |
better type reconstruction -- prevents ill-instantiations in proof replay
|
file |
diff |
annotate
|
| Thu, 15 Sep 2011 10:57:40 +0200 |
blanchet |
tuning
|
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
| base
|