src/HOL/Tools/code_evaluation.ML
2011-11-09 wenzelm 2011-11-09 tuned signature; tuned;
2011-11-05 wenzelm 2011-11-05 added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types; tuned;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-04-19 wenzelm 2011-04-19 simplified check/uncheck interfaces: result comparison is hardwired by default; tuned;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-17 haftmann 2010-12-17 avoid slightly odd Conv.tap_thy
2010-12-15 haftmann 2010-12-15 simplified evaluation function names
2010-11-26 haftmann 2010-11-26 keep type variable arguments of datatype constructors in bookkeeping
2010-09-20 haftmann 2010-09-20 dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
2010-09-20 haftmann 2010-09-20 full palette of dynamic/static value(_strict/exn)
2010-09-20 haftmann 2010-09-20 Factored out ML into separate file