| Fri, 20 Aug 2010 14:15:29 +0200 | blanchet | improve "x = A | x = B | x = C"-style fact discovery | changeset | files |
| Fri, 20 Aug 2010 14:09:02 +0200 | blanchet | transform elim theorems before filtering "bool" and "prop" variables out; | changeset | files |
| Fri, 20 Aug 2010 13:39:47 +0200 | blanchet | more fiddling with Sledgehammer's "add:" option | changeset | files |