src/HOL/Tools/recfun_codegen.ML
2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-02-19 ago using Code.bare_thms_of_cert
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
2009-11-08 ago adapted Theory_Data;
2009-10-27 ago Datatype.read_typ: standard argument order;
2009-10-15 ago replaced String.concat by implode;
2009-10-14 ago more explicit notion of canonized code equations
2009-08-11 ago proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
2009-08-10 ago moved all technical processing of code equations to code_thingol.ML
2009-07-31 ago cleaned up variable desymbolification and argument expansion
2009-07-14 ago code attributes use common underscore convention
2009-07-08 ago tuned structure Code internally
2009-07-07 ago merged
2009-07-07 ago tuned interface of structure Code
2009-07-07 ago Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
2009-05-14 ago merged module code_unit.ML into code.ML
2009-05-12 ago transferred code generator preprocessor into separate module
2009-05-11 ago clarified matter of "proper" flag in code equations
2009-05-11 ago simplified unoverload/overload policy in code generator preprocessor
2009-05-04 ago removed code_name module
2009-03-01 ago use long names for old-style fold combinators;
2008-12-31 ago use regular Term.add_XXX etc.;
2008-10-28 ago cleanup code default attribute
2008-10-09 ago made SMLNJ happy
2008-10-07 ago only one theorem table for both code generators
2008-09-26 ago removed obsolete name convention "func"
2008-06-30 ago simplified retrieval of theory names of consts and types
2008-05-23 ago Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
2008-05-17 ago structure Display: less pervasive operations;
2008-01-13 ago Equations for constants without arguments are now declared using
2007-12-07 ago proper treatment of code theorems for primrec
2007-11-11 ago renamed Symtab.update_list to Symtab.cons_list;
2007-10-08 ago Codegen.is_instance: raw match, ignore sort constraints;
2007-09-18 ago distinction between regular and default code theorems
2007-09-15 ago fixed title
2007-08-10 ago new structure for code generator modules
2007-05-10 ago consts in consts_code Isar commands are now referred to by usual term syntax
2007-05-09 ago tuned
2007-05-07 ago simplified DataFun interfaces;
2007-03-20 ago improved treatment of defining equations stemming from specification tools
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-11-18 ago tuned
2006-10-31 ago introduced CodegenData.add_func_legacy
2006-10-10 ago gen_rem(s) abandoned in favour of remove / subtract
2006-10-09 ago attribute: Context.mapping;
2006-09-22 ago Replaced irreducible_paths by all_paths.
2006-09-19 ago code generation 2 adjustments
2006-06-06 ago deleted legacy
2006-05-09 ago adaption to CodegenTheorems
2006-05-05 ago replaced Graph.find_paths by Graph.irreducible_paths;
2006-04-06 ago added hook for codegen_theorems.ML
2006-03-07 ago substantial improvement in codegen iml
2006-02-06 ago TableFun: renamed xxx_multi to xxx_list;
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-17 ago substantial improvements in code generator
2005-11-22 ago added codegenerator
2005-09-15 ago TableFun/Symtab: curried lookup and update;