| Thu, 12 May 2011 15:29:19 +0200 | blanchet | reduced penalty associated with existential quantifiers | changeset | files |
| Thu, 12 May 2011 15:29:19 +0200 | blanchet | ensure that Auto Sledgehammer is run with full type information | changeset | files |
| Thu, 12 May 2011 15:29:19 +0200 | blanchet | fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized | changeset | files |
| Thu, 12 May 2011 15:29:19 +0200 | blanchet | don't give weights to built-in symbols | changeset | files |
| Thu, 12 May 2011 15:29:19 +0200 | blanchet | more robust exception handling in Metis (also works if there are several subgoals) | changeset | files |
| Thu, 12 May 2011 15:29:19 +0200 | blanchet | no penality for constants that appear in chained facts | changeset | files |
| Thu, 12 May 2011 15:29:19 +0200 | blanchet | gracefully declare fTrue and fFalse proxies' types if the constants only appear in the helpers | changeset | files |