src/HOL/Tools/inductive_codegen.ML
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.