src/HOL/Tools/inductive_codegen.ML
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.
2004-09-23 berghofe 2004-09-23 - Inserted additional check for equality types in check_mode_clause that avoids ill-typed code to be generated. - Mode inference algorithm now outputs additional diagnostic messages.
2004-08-10 berghofe 2004-08-10 Fixed bug in compile_clause that caused equality constraints to be "forgotten".
2004-07-19 berghofe 2004-07-19 Added simple check that allows code generator to produce code containing fewer redundant matches.
2004-07-09 berghofe 2004-07-09 - Added support for conditional equations whose premises involve inductive sets (useful in connection with THE operator) - Inductive and non-inductive sets (implemented as lists) can now be mixed
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-01 berghofe 2004-06-01 Adapted to new name mangling function.
2004-04-14 berghofe 2004-04-14 Fixed bug in check_mode_clause.
2003-10-29 berghofe 2003-10-29 Inserted additional checks in functions dest_prem and add_prod_factors, to allow side conditions of the form "x : S", where S is not an inductive set.
2003-09-22 berghofe 2003-09-22 Changed interface of add_attribute.
2003-08-22 berghofe 2003-08-22 Improved handling of modes for equality predicate, to avoid ill-typed ML code due to comparisons between elements of function types.
2003-08-21 berghofe 2003-08-21 Fixed problem with "code ind" attribute that caused code generator to fail for mutually recursive predicates.
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
2002-03-07 berghofe 2002-03-07 - made modes_of more robust - assoc_code now has higher priority than inductive_codegen
2001-12-20 berghofe 2001-12-20 Eliminated "query" syntax.
2001-12-20 berghofe 2001-12-20 Fixed bug in function add.
2001-12-20 berghofe 2001-12-20 Implemented higher order modes.
2001-12-10 berghofe 2001-12-10 - Changed type of invoke_codegen - Added combinators for sequences
2001-08-31 wenzelm 2001-08-31 tuned headers;
2001-08-31 berghofe 2001-08-31 New code generators for HOL.