| 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 |
| Sun, 01 May 2011 18:37:24 +0200 | blanchet | fix handling of proxies after recent drastic changes to the type encodings | changeset | files |
| Sun, 01 May 2011 18:37:24 +0200 | blanchet | added a hint to Metis errors suggesting metisFT -- it sometimes work | changeset | files |
| Sun, 01 May 2011 18:37:24 +0200 | blanchet | reconstruct TFF type predicates correctly for ToFoF | changeset | files |
| Sun, 01 May 2011 18:37:24 +0200 | blanchet | fixed parsing of not in ATP proofs (e.g. ~x | y is (~x) | y, not ~(x | y)) | changeset | files |