src/HOL/Tools/recfun_codegen.ML
2009-08-11 haftmann 2009-08-11 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
2009-08-10 haftmann 2009-08-10 moved all technical processing of code equations to code_thingol.ML
2009-07-31 haftmann 2009-07-31 cleaned up variable desymbolification and argument expansion
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-07-08 haftmann 2009-07-08 tuned structure Code internally
2009-07-07 haftmann 2009-07-07 merged
2009-07-07 haftmann 2009-07-07 tuned interface of structure Code
2009-07-07 haftmann 2009-07-07 Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
2009-05-14 haftmann 2009-05-14 merged module code_unit.ML into code.ML
2009-05-12 haftmann 2009-05-12 transferred code generator preprocessor into separate module
2009-05-11 haftmann 2009-05-11 clarified matter of "proper" flag in code equations
2009-05-11 haftmann 2009-05-11 simplified unoverload/overload policy in code generator preprocessor
2009-05-04 haftmann 2009-05-04 removed code_name module
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2008-12-31 wenzelm 2008-12-31 use regular Term.add_XXX etc.;
2008-10-28 haftmann 2008-10-28 cleanup code default attribute
2008-10-09 haftmann 2008-10-09 made SMLNJ happy
2008-10-07 haftmann 2008-10-07 only one theorem table for both code generators
2008-09-26 haftmann 2008-09-26 removed obsolete name convention "func"
2008-06-30 haftmann 2008-06-30 simplified retrieval of theory names of consts and types
2008-05-23 berghofe 2008-05-23 Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately.
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-01-13 berghofe 2008-01-13 Equations for constants without arguments are now declared using "val" instead of "fun".
2007-12-07 haftmann 2007-12-07 proper treatment of code theorems for primrec
2007-11-11 wenzelm 2007-11-11 renamed Symtab.update_list to Symtab.cons_list;
2007-10-08 wenzelm 2007-10-08 Codegen.is_instance: raw match, ignore sort constraints;
2007-09-18 haftmann 2007-09-18 distinction between regular and default code theorems
2007-09-15 haftmann 2007-09-15 fixed title
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-05-10 haftmann 2007-05-10 consts in consts_code Isar commands are now referred to by usual term syntax
2007-05-09 haftmann 2007-05-09 tuned
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-03-20 haftmann 2007-03-20 improved treatment of defining equations stemming from specification tools
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-11-18 haftmann 2006-11-18 tuned
2006-10-31 haftmann 2006-10-31 introduced CodegenData.add_func_legacy
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-10-09 wenzelm 2006-10-09 attribute: Context.mapping;
2006-09-22 berghofe 2006-09-22 Replaced irreducible_paths by all_paths.
2006-09-19 haftmann 2006-09-19 code generation 2 adjustments
2006-06-06 haftmann 2006-06-06 deleted legacy
2006-05-09 haftmann 2006-05-09 adaption to CodegenTheorems
2006-05-05 wenzelm 2006-05-05 replaced Graph.find_paths by Graph.irreducible_paths;
2006-04-06 haftmann 2006-04-06 added hook for codegen_theorems.ML
2006-03-07 haftmann 2006-03-07 substantial improvement in codegen iml
2006-02-06 wenzelm 2006-02-06 TableFun: renamed xxx_multi to xxx_list;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2005-11-22 haftmann 2005-11-22 added codegenerator
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-08-25 berghofe 2005-08-25 Implemented incremental code generation.
2005-07-01 berghofe 2005-07-01 Adapted to modular code generation.
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun;
2005-04-12 paulson 2005-04-12 tweaks mainly to achieve sml/nj compatibility
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.