Thu, 16 Dec 2010 15:44:32 +0100 | blanchet | removed unused variable | changeset | files |
Thu, 16 Dec 2010 15:12:17 +0100 | blanchet | robustly handle SMT exceptions in Sledgehammer | changeset | files |
Thu, 16 Dec 2010 15:12:17 +0100 | blanchet | make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive | changeset | files |
Thu, 16 Dec 2010 15:12:17 +0100 | blanchet | reintroduce the higher penalty for skolems | changeset | files |