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
|