src/HOL/Tools/code_evaluation.ML
2017-08-03 haftmann 2017-08-03 one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy
2017-08-02 haftmann 2017-08-02 simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping; sufficient to keep history stamps rather than complete historized data; semantically conflicting specifications are temoprary blacklisted after theory merge but remain historized; clarified signature;
2017-07-02 haftmann 2017-07-02 proper concept of code declaration wrt. atomicity and Isar declarations
2017-02-28 haftmann 2017-02-28 stripped unused / obsolete material
2016-08-05 wenzelm 2016-08-05 more tight filtering;
2016-06-06 haftmann 2016-06-06 explicit tagging of code equations de-baroquifies interface
2016-05-29 wenzelm 2016-05-29 clarified check_open_spec / read_open_spec; allow 'for' fixes in 'abbreviation', 'definition';
2016-05-26 haftmann 2016-05-26 delegate inclusion of required dictionaries to user-space instead of half-working magic
2016-05-26 haftmann 2016-05-26 clarified naming conventions and code for code evaluation sandwiches
2016-04-28 wenzelm 2016-04-28 support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
2016-04-11 wenzelm 2016-04-11 tuned;
2015-11-15 haftmann 2015-11-15 droppen diagnostic junk from 4b53042d7a40
2015-11-14 haftmann 2015-11-14 explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-06 wenzelm 2015-03-06 tuned -- more explicit use of context;
2015-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2015-01-09 haftmann 2015-01-09 modernized and more uniform style
2014-12-19 wenzelm 2014-12-19 tuned;
2014-12-19 wenzelm 2014-12-19 proper exception for internal program failure, not user-error;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-05-15 haftmann 2014-05-15 syntactic means to prevent accidental mixup of static and dynamic context
2014-05-09 haftmann 2014-05-09 modernized setups
2014-05-09 haftmann 2014-05-09 degeneralized value command into HOL
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-26 haftmann 2014-02-26 prefer proof context over background theory
2013-04-18 haftmann 2013-04-18 spelling
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2012-07-16 wenzelm 2012-07-16 more direct Sorts.has_instance; tuned Sorts.mg_domain;
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