| Mon, 08 Sep 2014 14:03:13 +0200 | blanchet | compile | file | diff | annotate |
| Wed, 03 Sep 2014 22:47:09 +0200 | blanchet | intelligible errors instead of tactic failures | file | diff | annotate |
| Wed, 03 Sep 2014 22:47:05 +0200 | blanchet | made new tactic even more robust | file | diff | annotate |
| Wed, 03 Sep 2014 22:47:05 +0200 | blanchet | fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic) | file | diff | annotate |
| Wed, 03 Sep 2014 22:47:05 +0200 | blanchet | improved tactic further | file | diff | annotate |
| 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 |