| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
shorten readable names -- they can get really long with monomorphization, which actually slows down the ATPs
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
avoid Type.TYPE_MATCH exception for "True_or_False" for "If"
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
proper handling of partially applied proxy symbols
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
make the problems a bit lighter by getting rid of bound quantifiers for monomorphized constants, since these always have the same return type
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
improve helper type instantiation code
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
killed needless datatype "combtyp" in Metis
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
have properly type-instantiated helper facts (combinators and If)
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
don't destroy sym table entry for special symbols such as "hAPP" if "explicit_apply" is set
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
better known failure recognition for ToFoF-E
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
fixed min-arity computation when "explicit_apply" is specified
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
fixed "tags" type encoding after latest round of changes
|
changeset |
files
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
more higher-order tests for Sledgehammer/ATP
|
changeset |
files
|