src/HOL/Tools/recfun_codegen.ML
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-05-05 haftmann 2010-05-05 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 haftmann 2010-02-19 using Code.bare_thms_of_cert
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
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-27 wenzelm 2009-10-27 Datatype.read_typ: standard argument order; eliminated some old folds;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-10-14 haftmann 2009-10-14 more explicit notion of canonized code equations
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