src/Tools/Code/code_preproc.ML
2011-12-29 haftmann 2011-12-29 semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
2011-10-21 bulwahn 2011-10-21 removing redundant attribute code_inline in the code generator
2011-10-19 bulwahn 2011-10-19 removing declaration of code_unfold to address the old code generator
2011-08-20 wenzelm 2011-08-20 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-06-01 bulwahn 2011-06-01 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 wenzelm 2011-04-18 pass plain Proof.context for pretty printing;
2011-04-18 wenzelm 2011-04-18 simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
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 clarified exports of structure Simplifier;
2010-12-16 haftmann 2010-12-16 more appropriate closures for static evaluation
2010-12-15 haftmann 2010-12-15 simplified evaluation function names
2010-10-26 haftmann 2010-10-26 tuned
2010-10-26 haftmann 2010-10-26 dropped accidental doubled computation
2010-09-21 haftmann 2010-09-21 avoid frees and vars in terms to be evaluated by abstracting and applying
2010-09-16 haftmann 2010-09-16 separation of static and dynamic thy context
2010-09-15 haftmann 2010-09-15 ignore code cache optionally; corrected scope of term value in static_eval_conv
2010-09-05 wenzelm 2010-09-05 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-09-01 haftmann 2010-09-01 repaired attribute code_unfold_post which has ever been broken
2010-08-23 haftmann 2010-08-23 dropped pre_post_conv
2010-08-23 haftmann 2010-08-23 added static_eval_conv
2010-08-23 haftmann 2010-08-23 refined and unified naming convention for dynamic code evaluation techniques
2010-08-09 haftmann 2010-08-09 minimize sorts in certificate instantiation
2010-07-08 haftmann 2010-07-08 tuned titles
2010-06-15 haftmann 2010-06-15 added code_simp infrastructure
2010-06-07 haftmann 2010-06-07 more consistent naming aroud type classes and instances
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-11 wenzelm 2010-04-11 of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-02-19 wenzelm 2010-02-19 merged
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-19 haftmann 2010-02-19 simplified
2010-01-13 haftmann 2010-01-13 explicit abstract type of code certificates
2010-01-13 haftmann 2010-01-13 function transformer preprocessor applies to both code generators
2010-01-12 haftmann 2010-01-12 code certificates as integral part of code generation
2010-01-04 haftmann 2010-01-04 code cache only persists on equal theories
2010-01-04 haftmann 2010-01-04 code cache without copy; tuned
2009-12-23 haftmann 2009-12-23 reduced code generator cache to the baremost minimum
2009-12-02 haftmann 2009-12-02 tuned
2009-11-15 wenzelm 2009-11-15 permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-10-05 haftmann 2009-10-05 tuned handling of type variable names further
2009-10-05 haftmann 2009-10-05 variables in type schemes must be renamed simultaneously with variables in equations
2009-09-30 wenzelm 2009-09-30 Sorts.of_sort_derivation: no pp here;
2009-09-09 haftmann 2009-09-09 moved eq handling in nbe into separate oracle
2009-08-10 haftmann 2009-08-10 moved all technical processing of code equations to code_thingol.ML
2009-08-10 haftmann 2009-08-10 attempt to move desymbolization to translation
2009-07-31 haftmann 2009-07-31 added a somehow clueless comment
2009-07-31 haftmann 2009-07-31 cleaned up variable desymbolification and argument expansion
2009-07-22 wenzelm 2009-07-22 merged, resolving trivial conflict;
2009-07-21 haftmann 2009-07-21 integrated add_triv_classes into evaluation stack
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-14 haftmann 2009-07-14 added code_unfold_post attribute
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2009-07-08 haftmann 2009-07-08 tuned structure Code internally
2009-07-07 haftmann 2009-07-07 tuned interface of structure Code