src/HOL/Code_Evaluation.thy
Tue, 16 Sep 2014 19:23:37 +0200 blanchet added 'extraction' plugins -- this might help 'HOL-Proofs'
Sun, 14 Sep 2014 22:59:30 +0200 blanchet disable datatype 'plugins' for internal types
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Wed, 03 Sep 2014 00:06:24 +0200 blanchet use 'datatype_new' in 'Main'
Mon, 25 Aug 2014 09:08:45 +0200 Andreas Lochbihler correct code equation for term_of on integer
Fri, 22 Aug 2014 14:39:40 +0200 Andreas Lochbihler add code equation for term_of on integer
less more (0) -30 -10 -6 tip