src/HOL/Tools/inductive_codegen.ML
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
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-07-30 haftmann 2009-07-30 path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
2009-07-29 haftmann 2009-07-29 cleaned up abstract tuple operations and named them consistently
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-29 haftmann 2009-06-29 explicit Set constructor for code generated for sets
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-01 wenzelm 2009-01-01 eliminated OldTerm.(add_)term_consts;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-10-09 haftmann 2008-10-09 established canonical argument order in SML code generators
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
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-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 cat_lines;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2007-09-18 haftmann 2007-09-18 separated code for inductive sequences from inductive_codegen.ML
2007-09-15 haftmann 2007-09-15 fixed title
2007-08-28 berghofe 2007-08-28 Added sequences with recursion depth limit.
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-08-02 berghofe 2007-08-02 - Added cycle test to function mk_ind_def to avoid non-termination of code generator. - Functions generated from inductive predicates having neither parameters nor input arguments now take a unit element as an argument, otherwise the generated code would be ill-formed.
2007-07-11 berghofe 2007-07-11 Improved code generator for Collect.
2007-05-10 haftmann 2007-05-10 consts in consts_code Isar commands are now referred to by usual term syntax
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-25 berghofe 2007-04-25 Moved function params_of to inductive_package.ML.
2007-04-13 berghofe 2007-04-13 Removed erroneous application of rev in get_clauses that caused introduction rules taken from the InductivePackage database to be in the wrong order.
2007-04-12 haftmann 2007-04-12 canonical merge operations
2007-03-31 berghofe 2007-03-31 Fixed bug in dest_prem: premises of the form "p x_1 ... x_n" (where p is a variable) are now treated as side conditions if p is not in the list of (global) parameters.
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2006-10-13 berghofe 2006-10-13 Moved old inductive package to old_inductive_package.ML
2006-10-09 wenzelm 2006-10-09 attribute: Context.mapping;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-06-12 wenzelm 2006-06-12 tuned Seq/Envir/Unify interfaces;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-12 wenzelm 2006-02-12 simplified TableFun.join;
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 wenzelm 2006-02-06 replaced Symtab.merge_multi by local merge_rules;
2006-02-06 haftmann 2006-02-06 subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-12-13 berghofe 2005-12-13 list_of_indset now also generates code for set type.
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-15 wenzelm 2005-07-15 tuned fold on terms;
2005-07-01 berghofe 2005-07-01 Adapted to modular code generation.
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun;
2005-04-07 wenzelm 2005-04-07 handle Option instead of OPTION;
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-10-26 berghofe 2004-10-26 Added call to Codegen.preprocess.