| Wed, 03 Sep 2014 22:47:05 +0200 | blanchet | improved new countability tactic | file | diff | annotate |
| Wed, 03 Sep 2014 22:47:05 +0200 | blanchet | 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems | file | diff | annotate |
| Wed, 03 Sep 2014 09:43:00 +0200 | blanchet | added compatibility function | file | diff | annotate |
| Wed, 03 Sep 2014 00:31:38 +0200 | blanchet | added countable tactic for new-style datatypes | file | diff | annotate |