blanchet [Thu, 26 Sep 2013 15:13:28 +0200] rev 53920
made tactic more robust in case somebody specified a discriminator for a one-constructor type
blanchet [Thu, 26 Sep 2013 13:56:07 +0200] rev 53919
tuning
blanchet [Thu, 26 Sep 2013 13:51:08 +0200] rev 53918
use new "sel_split(_asm)" to avoid giving rise to quantifiers, which would in turn require relying on injectivity
blanchet [Thu, 26 Sep 2013 13:42:14 +0200] rev 53917
generate "sel_splits(_asm)" theorems
blanchet [Thu, 26 Sep 2013 13:42:13 +0200] rev 53916
generate "sel_exhaust" theorem
wenzelm [Thu, 26 Sep 2013 13:34:42 +0200] rev 53915
merged
wenzelm [Thu, 26 Sep 2013 13:28:26 +0200] rev 53914
obsolete (see also 48d13465c7c7);
wenzelm [Thu, 26 Sep 2013 12:56:59 +0200] rev 53913
prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);
wenzelm [Thu, 26 Sep 2013 10:42:10 +0200] rev 53912
initialize class immediately (potentially more robust);
nipkow [Thu, 26 Sep 2013 11:41:01 +0200] rev 53911
tuned