src/HOL/Tools/datatype_codegen.ML
2007-08-24 haftmann 2007-08-24 overloaded definitions accompanied by explicit constants
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-08-03 wenzelm 2007-08-03 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-16 haftmann 2007-07-16 added function for case certificates
2007-07-10 haftmann 2007-07-10 tuned
2007-06-28 haftmann 2007-06-28 tuned
2007-05-10 haftmann 2007-05-10 consts in consts_code Isar commands are now referred to by usual term syntax
2007-04-24 berghofe 2007-04-24 Streamlined datatype_codegen function using new datatype_of_case and datatype_of_constr functions.
2007-04-20 haftmann 2007-04-20 cleared dead code
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2007-04-03 wenzelm 2007-04-03 ranamed CodegenData.lazy to lazy_thms (avoid clash with Alice keywords);
2007-03-30 haftmann 2007-03-30 simplified constant representation in code generator
2007-03-20 haftmann 2007-03-20 switched exception from arbitrary to undefined
2007-03-11 haftmann 2007-03-11 clarified code
2007-03-10 berghofe 2007-03-10 Eta-expanded codetype_hook to make SML/NJ happy.
2007-03-09 haftmann 2007-03-09 dropped code datatype certificates
2007-02-16 wenzelm 2007-02-16 unified arity parser/arguments;
2007-02-10 haftmann 2007-02-10 canonical interface for attributes
2007-01-25 haftmann 2007-01-25 adjusted names
2007-01-10 haftmann 2007-01-10 improved case patterns
2007-01-10 haftmann 2007-01-10 added undefined in cases
2007-01-09 haftmann 2007-01-09 handling for "undefined" in case expressions
2006-12-29 haftmann 2006-12-29 simplified class_package
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-11-28 wenzelm 2006-11-28 simplified '?' operator;
2006-11-27 haftmann 2006-11-27 removed HOL structure
2006-11-24 wenzelm 2006-11-24 ProofContext.init;
2006-11-22 haftmann 2006-11-22 dropped eq const
2006-10-16 haftmann 2006-10-16 moved HOL code generator setup to Code_Generator
2006-10-13 haftmann 2006-10-13 tuned
2006-10-04 haftmann 2006-10-04 clarified header comments
2006-10-02 haftmann 2006-10-02 tuned
2006-09-22 berghofe 2006-09-22 Fixed bug concerning the generation of identifiers for datatypes, which caused the code generator to fail for mutually recursive datatypes.
2006-09-19 haftmann 2006-09-19 removed diagnostic messages
2006-09-19 haftmann 2006-09-19 code generation 2 adjustments
2006-08-30 haftmann 2006-08-30 code refinements
2006-08-30 haftmann 2006-08-30 fixes
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