blanchet [Tue, 16 Sep 2014 19:23:37 +0200] rev 58352
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet [Tue, 16 Sep 2014 19:23:37 +0200] rev 58351
took out 'old_datatype' examples -- those just cause timeouts in Isatests
blanchet [Tue, 16 Sep 2014 19:23:37 +0200] rev 58350
added 'extraction' plugins -- this might help 'HOL-Proofs'
nipkow [Tue, 16 Sep 2014 18:42:33 +0200] rev 58349
added lemma
Andreas Lochbihler [Tue, 16 Sep 2014 16:04:08 +0200] rev 58348
add target language evaluators for the value command;
drop obsolete command eval_term
blanchet [Mon, 15 Sep 2014 18:12:09 +0200] rev 58347
tuning
blanchet [Mon, 15 Sep 2014 17:56:37 +0200] rev 58346
refactoring
blanchet [Mon, 15 Sep 2014 16:34:05 +0200] rev 58345
tuning
blanchet [Mon, 15 Sep 2014 16:14:14 +0200] rev 58344
set 'mono' attribute on 'rel_mono'
blanchet [Mon, 15 Sep 2014 16:11:01 +0200] rev 58343
'code' is needed for extraction datatype
blanchet [Mon, 15 Sep 2014 14:31:32 +0200] rev 58342
tuning
blanchet [Mon, 15 Sep 2014 12:30:06 +0200] rev 58341
removed accidental '@{print}'
blanchet [Mon, 15 Sep 2014 12:11:41 +0200] rev 58340
tuning
blanchet [Mon, 15 Sep 2014 11:54:47 +0200] rev 58339
more hints on how to port 'size'