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 |
Sun, 01 May 2011 18:37:24 +0200 | blanchet | added friendly hint when Isar proof is missing | changeset | files |