| 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 |
| Thu, 26 Sep 2013 12:56:59 +0200 | wenzelm | prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850); | changeset | files |
| Thu, 26 Sep 2013 10:42:10 +0200 | wenzelm | initialize class immediately (potentially more robust); | changeset | files |
| Thu, 26 Sep 2013 11:41:01 +0200 | nipkow | tuned | changeset | files |
| Thu, 26 Sep 2013 10:57:39 +0200 | blanchet | strengthen tactic | changeset | files |
| Thu, 26 Sep 2013 10:26:00 +0200 | blanchet | use needed case theorems | changeset | files |
| Thu, 26 Sep 2013 10:20:23 +0200 | blanchet | tuning | changeset | files |
| Thu, 26 Sep 2013 10:00:07 +0200 | blanchet | added data query function | changeset | files |
| Thu, 26 Sep 2013 09:58:36 +0200 | blanchet | added data query function | changeset | files |
| Thu, 26 Sep 2013 02:34:34 +0200 | blanchet | tuning | changeset | files |
| Thu, 26 Sep 2013 02:25:33 +0200 | blanchet | got rid of dependency on silly 'eq_ifI' theorem | changeset | files |
| Thu, 26 Sep 2013 02:09:52 +0200 | blanchet | more powerful/robust tactics | changeset | files |
| Thu, 26 Sep 2013 01:05:32 +0200 | blanchet | use standard "split" properties instead of ad hoc "eq_...I" | changeset | files |
| Thu, 26 Sep 2013 01:05:07 +0200 | blanchet | tuning | changeset | files |
| Thu, 26 Sep 2013 01:05:06 +0200 | blanchet | made tactic more flexible w.r.t. case expressions and such | changeset | files |