src/HOL/Tools/datatype_codegen.ML
2007-12-10 ago moved instance parameter management from class.ML to axclass.ML
2007-12-07 ago dropped Instance.instantiate
2007-12-05 ago simplified infrastructure for code generator operational equality
2007-11-29 ago stripped down
2007-11-29 ago instance command as rudimentary class target
2007-11-28 ago simplified interpretations
2007-11-28 ago tuned interfaces of class module
2007-10-11 ago moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
2007-10-04 ago tuned datatype_codegen setup
2007-09-25 ago simplified interpretation setup;
2007-09-25 ago datatype interpretators for size and datatype_realizer
2007-09-18 ago introduced generic concepts for theory interpretators
2007-09-18 ago distinction between regular and default code theorems
2007-09-15 ago clarified class interfaces and internals
2007-08-25 ago made SML/NJ happy
2007-08-24 ago overloaded definitions accompanied by explicit constants
2007-08-10 ago new structure for code generator modules
2007-08-03 ago replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-16 ago added function for case certificates
2007-07-10 ago tuned
2007-06-28 ago tuned
2007-05-10 ago consts in consts_code Isar commands are now referred to by usual term syntax
2007-04-24 ago Streamlined datatype_codegen function using new datatype_of_case
2007-04-20 ago cleared dead code
2007-04-04 ago removed obsolete sign_of/sign_of_thm;
2007-04-03 ago ranamed CodegenData.lazy to lazy_thms (avoid clash with Alice keywords);
2007-03-30 ago simplified constant representation in code generator
2007-03-20 ago switched exception from arbitrary to undefined
2007-03-11 ago clarified code
2007-03-10 ago Eta-expanded codetype_hook to make SML/NJ happy.
2007-03-09 ago dropped code datatype certificates
2007-02-16 ago unified arity parser/arguments;
2007-02-10 ago canonical interface for attributes
2007-01-25 ago adjusted names
2007-01-10 ago improved case patterns
2007-01-10 ago added undefined in cases
2007-01-09 ago handling for "undefined" in case expressions
2006-12-29 ago simplified class_package
2006-12-07 ago reorganized structure Tactic vs. MetaSimplifier;
2006-11-28 ago simplified '?' operator;
2006-11-27 ago removed HOL structure
2006-11-24 ago ProofContext.init;
2006-11-22 ago dropped eq const
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