| Thu, 26 Sep 2013 16:50:40 +0200 | Andreas Lochbihler | merged | changeset | files |
| Thu, 26 Sep 2013 15:50:33 +0200 | Andreas Lochbihler | add lemmas | changeset | files |
| Thu, 26 Sep 2013 16:41:32 +0200 | blanchet | strengthened tactic | changeset | files |
| Thu, 26 Sep 2013 16:25:12 +0200 | blanchet | tuning | changeset | files |
| Thu, 26 Sep 2013 16:17:34 +0200 | blanchet | avoid calls to nth with ~1 | changeset | files |
| Thu, 26 Sep 2013 16:10:57 +0200 | blanchet | tuning | changeset | files |
| Thu, 26 Sep 2013 16:00:18 +0200 | blanchet | strengthened tactic | changeset | files |
| Thu, 26 Sep 2013 15:13:55 +0200 | blanchet | tactic cleanup | changeset | files |
| Thu, 26 Sep 2013 15:13:28 +0200 | blanchet | made tactic more robust in case somebody specified a discriminator for a one-constructor type | changeset | files |
| Thu, 26 Sep 2013 13:56:07 +0200 | blanchet | tuning | changeset | files |
| Thu, 26 Sep 2013 13:51:08 +0200 | blanchet | use new "sel_split(_asm)" to avoid giving rise to quantifiers, which would in turn require relying on injectivity | changeset | files |
| Thu, 26 Sep 2013 13:42:14 +0200 | blanchet | generate "sel_splits(_asm)" theorems | changeset | files |
| Thu, 26 Sep 2013 13:42:13 +0200 | blanchet | generate "sel_exhaust" theorem | changeset | files |
| Thu, 26 Sep 2013 13:34:42 +0200 | wenzelm | merged | changeset | files |
| Thu, 26 Sep 2013 13:28:26 +0200 | wenzelm | obsolete (see also 48d13465c7c7); | changeset | files |