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