Andreas Lochbihler [Tue, 24 Sep 2013 11:33:56 +0200] rev 53817
merged
Andreas Lochbihler [Tue, 24 Sep 2013 10:35:37 +0200] rev 53816
make measure_of total
blanchet [Tue, 24 Sep 2013 11:02:42 +0200] rev 53815
encode goal digest in spying log (to detect duplicates)
blanchet [Tue, 24 Sep 2013 09:12:09 +0200] rev 53814
made SML/NJ happy
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