| 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 |