src/Tools/Code/code_simp.ML
2021-10-20 wenzelm discontinued obsolete "val extend = I" for data slots;
2019-01-04 wenzelm isabelle update -u control_cartouches;
2016-05-26 haftmann optional timing for code generator conversions
2016-05-26 haftmann corrected closure scope of static_conv_thingol;
2016-05-26 haftmann clarified names of variants
2015-03-06 wenzelm clarified context;
2015-03-06 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-01-09 haftmann modernized and more uniform style
2014-05-15 haftmann syntactic means to prevent accidental mixup of static and dynamic context
2014-05-15 haftmann dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
2014-05-09 haftmann dimiss simplified as evaluator due to little practical relevance
2014-05-09 haftmann normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
2014-05-01 haftmann cleanup
2014-02-26 haftmann prefer proof context over background theory
2014-01-25 haftmann prefer explicit code symbol type over ad-hoc name mangling
2014-01-03 haftmann proper context for simplifier invocations in code generation stack
2014-01-03 haftmann spelling
2014-01-01 wenzelm clarified simplifier context;
2013-09-06 haftmann tuned
2013-08-22 haftmann separate tracing option for code_simp
2013-07-27 haftmann more correct context for dynamic invocations of static code conversions etc.
2013-04-18 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
2012-06-05 haftmann prefer records with speaking labels over deeply nested tuples
2012-04-19 haftmann dropped dead code;
2011-11-23 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-07-01 wenzelm proper @{binding} antiquotations (relevant for formal references);
2011-04-16 wenzelm modernized structure Proof_Context;
2010-12-21 haftmann canonical handling of theory context argument
2010-12-17 wenzelm merged
2010-12-17 haftmann avoid slightly odd Conv.tap_thy
2010-12-17 wenzelm refer to regular structure Simplifier;
2010-12-16 haftmann more uniform naming
2010-12-15 haftmann simplified evaluation function names
2010-09-21 haftmann no_frees_* is subsumed by new framework mechanisms in Code_Preproc
2010-09-21 haftmann more conventional conversion signature
2010-09-17 haftmann refined static_eval_conv_simple; tuned comments
2010-09-16 haftmann separation of static and dynamic thy context
2010-08-26 wenzelm simplification/standardization of some theory data;
2010-08-23 haftmann use Code_Thingol.static_eval_conv_simple
2010-08-23 haftmann refined and unified naming convention for dynamic code evaluation techniques
2010-07-16 haftmann tuned interpunctation
2010-07-08 haftmann tuned titles
2010-06-18 haftmann code_simp: only succeed on real progress
2010-06-18 haftmann conclude simplification with default simpset
2010-06-17 haftmann more precise code
2010-06-17 haftmann added simp evaluator
2010-06-15 haftmann added code_simp infrastructure
less more (0) tip