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