2014-03-31 ago some shortcuts for chunks, which sometimes avoid bulky string output;
2014-02-26 ago prefer proof context over background theory
2014-02-09 ago build up preprocessing context only once
2014-01-03 ago proper context for simplifier invocations in code generation stack
2014-01-01 ago clarified simplifier context;
2013-09-06 ago tuned
2013-07-27 ago more correct context for dynamic invocations of static code conversions etc.
2013-04-18 ago simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 ago more standard module name Axclass (according to file name);
2013-04-09 ago discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
2012-10-22 ago close code theorems explicitly after preprocessing
2012-06-05 ago apply preprocessing simpset also to rhs of abstract code equations
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-03-16 ago outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-02-15 ago renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-12-29 ago semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
2011-10-21 ago removing redundant attribute code_inline in the code generator
2011-10-19 ago removing declaration of code_unfold to address the old code generator
2011-08-20 ago refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-06-01 ago code preprocessor applies simplifier when schematic variables are fixed to free variables to allow rewriting with congruence rules in the preprocessing steps
2011-04-18 ago pass plain Proof.context for pretty printing;
2011-04-18 ago simplified pretty printing context, which is only required for certain kernel operations;
2011-04-16 ago modernized structure Proof_Context;
2010-12-21 ago canonical handling of theory context argument
2010-12-17 ago clarified exports of structure Simplifier;
2010-12-16 ago more appropriate closures for static evaluation
2010-12-15 ago simplified evaluation function names
2010-10-26 ago tuned
2010-10-26 ago dropped accidental doubled computation
2010-09-21 ago avoid frees and vars in terms to be evaluated by abstracting and applying
2010-09-16 ago separation of static and dynamic thy context
2010-09-15 ago ignore code cache optionally; corrected scope of term value in static_eval_conv
2010-09-05 ago pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-09-01 ago repaired attribute code_unfold_post which has ever been broken
2010-08-23 ago dropped pre_post_conv
2010-08-23 ago added static_eval_conv
2010-08-23 ago refined and unified naming convention for dynamic code evaluation techniques
2010-08-09 ago minimize sorts in certificate instantiation
2010-07-08 ago tuned titles
2010-06-15 ago added code_simp infrastructure
2010-06-07 ago more consistent naming aroud type classes and instances
2010-05-17 ago prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-11 ago of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
2010-03-07 ago modernized structure Local_Defs;
2010-02-19 ago merged
2010-02-19 ago renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-19 ago simplified
2010-01-13 ago explicit abstract type of code certificates
2010-01-13 ago function transformer preprocessor applies to both code generators
2010-01-12 ago code certificates as integral part of code generation
2010-01-04 ago code cache only persists on equal theories
2010-01-04 ago code cache without copy; tuned
2009-12-23 ago reduced code generator cache to the baremost minimum
2009-12-02 ago tuned
2009-11-15 ago permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);
2009-11-08 ago adapted Theory_Data;
2009-10-22 ago map_range (and map_index) combinator
2009-10-05 ago tuned handling of type variable names further
2009-10-05 ago variables in type schemes must be renamed simultaneously with variables in equations