Wed, 03 Sep 2014 22:47:05 +0200 | blanchet | reenabled example | changeset | files |
Wed, 03 Sep 2014 22:47:05 +0200 | blanchet | improved new countability tactic | changeset | files |
Wed, 03 Sep 2014 22:47:05 +0200 | blanchet | 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems | changeset | files |