huffman [Mon, 23 Sep 2013 16:56:17 -0700] rev 53813
tuned proofs
blanchet [Tue, 24 Sep 2013 00:21:40 +0200] rev 53812
use forthcoming "primcorec" command
blanchet [Tue, 24 Sep 2013 00:18:22 +0200] rev 53811
set code and nitpick_simp attributes on primcorec theorems
blanchet [Tue, 24 Sep 2013 00:10:59 +0200] rev 53810
tuning
blanchet [Tue, 24 Sep 2013 00:10:46 +0200] rev 53809
tuned docs
blanchet [Tue, 24 Sep 2013 00:01:10 +0200] rev 53808
register codatatypes with Nitpick
blanchet [Mon, 23 Sep 2013 23:27:46 +0200] rev 53807
register codatatypes with Nitpick
blanchet [Mon, 23 Sep 2013 18:40:02 +0200] rev 53806
don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)
blanchet [Mon, 23 Sep 2013 17:43:23 +0200] rev 53805
added [code] to selectors
blanchet [Mon, 23 Sep 2013 14:53:43 +0200] rev 53804
tuned spying
blanchet [Mon, 23 Sep 2013 14:53:43 +0200] rev 53803
document "spy"
blanchet [Mon, 23 Sep 2013 14:53:43 +0200] rev 53802
added "spy" option to Nitpick
blanchet [Mon, 23 Sep 2013 14:53:43 +0200] rev 53801
document "spy" option
blanchet [Mon, 23 Sep 2013 14:53:43 +0200] rev 53800
added "spy" option to Sledgehammer
wenzelm [Mon, 23 Sep 2013 13:34:15 +0200] rev 53799
proper text for document preparation;
blanchet [Mon, 23 Sep 2013 12:40:34 +0200] rev 53798
set [code] on case equations