| Mon, 23 Aug 2010 14:54:17 +0200 | blanchet | perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later; | changeset | files |
| Mon, 23 Aug 2010 14:51:56 +0200 | blanchet | "no_atp" fact that leads to unsound Sledgehammer proofs | changeset | files |
| Mon, 23 Aug 2010 14:21:57 +0200 | blanchet | "no_atp" fact that leads to unsound proofs in Sledgehammer | changeset | files |