src/HOL/Code_Evaluation.thy
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Sun, 02 Jun 2013 07:46:40 +0200 haftmann make reification part of HOL
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Fri, 15 Feb 2013 11:47:33 +0100 haftmann systematic conversions between nat and nibble/char;
Fri, 15 Feb 2013 08:31:31 +0100 haftmann less customary term_of conversions;
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Thu, 14 Feb 2013 15:27:10 +0100 haftmann reform of predicate compiler / quickcheck theories:
Thu, 14 Feb 2013 12:24:42 +0100 haftmann abandoned theory Plain
Mon, 12 Nov 2012 23:24:40 +0100 haftmann tuned import order
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Fri, 24 Feb 2012 22:46:44 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Fri, 24 Feb 2012 09:40:02 +0100 haftmann given up disfruitful branch
Thu, 23 Feb 2012 21:25:59 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Thu, 26 May 2011 09:42:02 +0200 bulwahn extending terms of Code_Evaluation by Free to allow partial terms
Thu, 02 Dec 2010 14:34:38 +0100 haftmann corrected representation for code_numeral numerals
Thu, 02 Dec 2010 13:53:36 +0100 haftmann separate term_of function for integers -- more canonical representation of negative integers
Mon, 22 Nov 2010 10:41:57 +0100 bulwahn adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
Mon, 20 Sep 2010 18:43:23 +0200 haftmann dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
Mon, 20 Sep 2010 15:10:21 +0200 haftmann Factored out ML into separate file
Thu, 16 Sep 2010 16:51:33 +0200 haftmann adjusted to changes in Code_Runtime
Wed, 15 Sep 2010 15:40:35 +0200 haftmann Code_Runtime.value, corresponding to ML_Context.value
Wed, 15 Sep 2010 15:31:32 +0200 haftmann code_eval renamed to code_runtime
Wed, 15 Sep 2010 11:30:31 +0200 haftmann replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
Fri, 10 Sep 2010 10:59:09 +0200 bulwahn fiddling with the correct setup for String.literal
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Wed, 11 Aug 2010 14:31:43 +0200 haftmann moved instantiation target formally to class_target.ML
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
less more (0) -30 tip