| Wed, 18 Aug 2010 18:01:54 +0200 | blanchet | minor cleanup | changeset | files |
| Wed, 18 Aug 2010 17:53:12 +0200 | blanchet | bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq") | changeset | files |
| Wed, 18 Aug 2010 17:23:17 +0200 | blanchet | update docs | changeset | files |
| Wed, 18 Aug 2010 17:16:37 +0200 | blanchet | get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize" | changeset | files |
| Wed, 18 Aug 2010 17:09:05 +0200 | blanchet | added "max_relevant_per_iter" option to Sledgehammer | changeset | files |
| Wed, 18 Aug 2010 16:42:37 +0200 | blanchet | thank Andrei instead of Tanya | changeset | files |
| Wed, 18 Aug 2010 16:39:05 +0200 | blanchet | fix the relevance filter so that it ignores If, Ex1, Ball, Bex | changeset | files |