| Thu, 26 Aug 2010 17:27:29 +0200 | blanchet | avoid needless "that" fact | changeset | files |
| Thu, 26 Aug 2010 16:18:40 +0200 | blanchet | add nameless chained facts to the pool of things known to Sledgehammer | changeset | files |
| Thu, 26 Aug 2010 14:58:45 +0200 | blanchet | if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem | changeset | files |