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 |