| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
|
changeset |
files
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
fixed eta-extension of higher-order quantifiers in THF output
|
changeset |
files
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
renamed "smt_fixed" to "smt_read_only_certificates"
|
changeset |
files
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
tuning (in particular, Symtab instead of AList)
|
changeset |
files
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
tweak slices, based on eval by Daniel Wand
|
changeset |
files
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
|
changeset |
files
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
print a hint
|
changeset |
files
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
avoid DL
|
changeset |
files
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
TFF: declare free types as types
|
changeset |
files
|
| Tue, 27 Mar 2012 15:34:04 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Tue, 27 Mar 2012 14:14:46 +0200 |
bulwahn |
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
|
changeset |
files
|
| Tue, 27 Mar 2012 14:49:56 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Tue, 27 Mar 2012 12:42:54 +0200 |
huffman |
move int::ring_div instance upward, simplify several proofs
|
changeset |
files
|