| Fri, 20 May 2011 12:47:58 +0200 | blanchet | generate useful information for type axioms | changeset | files |
| Fri, 20 May 2011 12:47:58 +0200 | blanchet | slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous | changeset | files |
| Fri, 20 May 2011 12:47:58 +0200 | blanchet | updated FAQ | changeset | files |
| Fri, 20 May 2011 12:47:58 +0200 | blanchet | more informative message when Sledgehammer finds an unsound proof | changeset | files |