src/HOL/Tools/datatype_codegen.ML
2006-10-16 ago moved HOL code generator setup to Code_Generator
2006-10-13 ago tuned
2006-10-04 ago clarified header comments
2006-10-02 ago tuned
2006-09-22 ago Fixed bug concerning the generation of identifiers for
2006-09-19 ago removed diagnostic messages
2006-09-19 ago code generation 2 adjustments
2006-08-30 ago code refinements
2006-08-30 ago fixes
2006-08-29 ago added typecopy_package
2006-08-17 ago cleanup
2006-08-14 ago added add_hook_bootstrap
2006-07-25 ago renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum
2006-07-25 ago fixed typo
2006-07-23 ago tactic for prove_instance_arity now gets definition theorems as arguments
2006-07-21 ago hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
2006-07-12 ago adaptions in codegen
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-06-14 ago added hook for case const defs
2006-06-07 ago adding case theorems for code generator
2006-05-09 ago added DatatypeHooks
2006-04-24 ago more precise tactics
2006-04-06 ago cleanup in datatype package
2006-02-10 ago improved code generator devarification
2006-02-07 ago slight improvements in code generation
2006-01-31 ago minor change to CodegenPackage interface
2006-01-19 ago setup: theory -> theory;
2006-01-17 ago substantial improvements in code generator
2005-12-29 ago adaptions to changes in code generator
2005-12-21 ago slight clean ups
2005-12-12 ago improvement in eq handling
2005-12-09 ago improved extraction interface
2005-12-02 ago adjusted to improved code generator interface
2005-11-25 ago code generator: case expressions, improved name resolving
2005-11-22 ago added codegenerator
2005-09-20 ago introduced AList module in favor of assoc etc.
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-05 ago curried_lookup/update;
2005-08-25 ago Implemented incremental code generation.
2005-07-01 ago Adapted to modular code generation.
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-12-10 ago Fixed bug in mk_gen_of_def that could cause non-termination of the generator
2004-06-21 ago Merged in license change from Isabelle2004
2003-07-11 ago Added generator for test case generators.
2002-12-16 ago Code generator for datatypes now also generates suitable term_of functions (when
2002-02-14 ago made MLWorks happy;
2002-01-21 ago datatype_codegen now checks type of constructor.
2001-12-10 ago Tuned header.
2001-12-10 ago Code generator for datatypes.