src/HOL/Tools/datatype_codegen.ML
2006-08-29 haftmann 2006-08-29 added typecopy_package
2006-08-17 haftmann 2006-08-17 cleanup
2006-08-14 haftmann 2006-08-14 added add_hook_bootstrap
2006-07-25 haftmann 2006-07-25 renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum
2006-07-25 haftmann 2006-07-25 fixed typo
2006-07-23 haftmann 2006-07-23 tactic for prove_instance_arity now gets definition theorems as arguments
2006-07-21 haftmann 2006-07-21 hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
2006-07-12 haftmann 2006-07-12 adaptions in codegen
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-06-14 haftmann 2006-06-14 added hook for case const defs
2006-06-07 haftmann 2006-06-07 adding case theorems for code generator
2006-05-09 haftmann 2006-05-09 added DatatypeHooks
2006-04-24 haftmann 2006-04-24 more precise tactics
2006-04-06 haftmann 2006-04-06 cleanup in datatype package
2006-02-10 haftmann 2006-02-10 improved code generator devarification
2006-02-07 haftmann 2006-02-07 slight improvements in code generation
2006-01-31 haftmann 2006-01-31 minor change to CodegenPackage interface
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2005-12-29 haftmann 2005-12-29 adaptions to changes in code generator
2005-12-21 haftmann 2005-12-21 slight clean ups
2005-12-12 haftmann 2005-12-12 improvement in eq handling
2005-12-09 haftmann 2005-12-09 improved extraction interface
2005-12-02 haftmann 2005-12-02 adjusted to improved code generator interface
2005-11-25 haftmann 2005-11-25 code generator: case expressions, improved name resolving
2005-11-22 haftmann 2005-11-22 added codegenerator
2005-09-20 haftmann 2005-09-20 introduced AList module in favor of assoc etc.
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-25 berghofe 2005-08-25 Implemented incremental code generation.
2005-07-01 berghofe 2005-07-01 Adapted to modular code generation.
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.
2004-12-10 berghofe 2004-12-10 Fixed bug in mk_gen_of_def that could cause non-termination of the generator for datatypes with nested recursion (such as trie).
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2003-07-11 berghofe 2003-07-11 Added generator for test case generators.
2002-12-16 berghofe 2002-12-16 Code generator for datatypes now also generates suitable term_of functions (when term_of mode is switched on).
2002-02-14 wenzelm 2002-02-14 made MLWorks happy;
2002-01-21 berghofe 2002-01-21 datatype_codegen now checks type of constructor.
2001-12-10 berghofe 2001-12-10 Tuned header.
2001-12-10 berghofe 2001-12-10 Code generator for datatypes.