src/HOL/Tools/recdef_package.ML
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago generic attributes;
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 ago oriented result pairs in PureThy
2005-10-19 ago removed obsolete add_recdef_old;
2005-09-23 ago temporarily re-introduced overwrite_warn
2005-09-21 ago introduces update_warn instead of overwrite_warn
2005-09-20 ago slight adaptions to library changes
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-13 ago tuned IsarThy.theorem_i;
2005-09-05 ago curried_lookup/update;
2005-08-16 ago OuterKeyword;
2005-07-01 ago Adapted to new interface of RecfunCodegen.add.
2005-06-17 ago accomodate change of TheoryDataFun;
2005-06-11 ago refer to name spaces values instead of names;
2005-05-31 ago renamed cond_extern to extern;
2005-04-13 ago *** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13 ago *** empty log message ***
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-01-24 ago Replaced xstring by thmref.
2004-07-11 ago local_cla/simpset_of;
2004-06-21 ago Merged in license change from Isabelle2004
2003-10-17 ago Prevent recdef from looping when the inductio rule is simplified
2002-02-12 ago got rid of explicit marginal comments (now stripped earlier from input);
2002-01-15 ago removed case_numbers (already covered by default);
2002-01-11 ago clarified IsarThy.apply_theorems_i;
2002-01-10 ago simplified IsarThy.theorem_i;
2001-12-10 ago Recursive equations to be used for code generation are now registered
2001-12-05 ago tuned;
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-08 ago theory data: finish method;
2001-11-04 ago IsarThy.theorem_i (None, []);
2001-10-31 ago IsarThy.theorem_i: no locale;
2001-10-13 ago IsarThy.theorem_i Drule.internalK;
2001-09-28 ago permissive option;
2001-01-03 ago added recdef_tc(_i);
2000-10-19 ago added tcs_of;
2000-09-19 ago tuned;
2000-09-15 ago added "congs" keyword;
2000-09-15 ago "hints" made keyword again;
2000-09-13 ago tuned recdef hints;
2000-09-07 ago tuned msg;
2000-09-06 ago make SML/NJ happy;
2000-09-06 ago tuned;
2000-09-05 ago recdef hints (attributes and modifiers);
2000-08-18 ago removed obsolete add_recdef_x;
2000-08-17 ago installed recdef congs data
2000-04-18 ago removed obsolete "simpset" keyword;
2000-04-13 ago outer syntax: no simps;
2000-04-01 ago recdef: admit names/atts;
2000-03-30 ago If all termination conditions are proved automatically,
2000-03-15 ago get_recdef now returns None instead of raising ERROR.
2000-03-13 ago adapted to new PureThy.add_thms etc.;
1999-10-08 ago return stored thms with proper naming in derivation;
1999-08-18 ago from Konrad: support for schematic definitions
1999-06-28 ago cond_extern_table;
1999-05-25 ago formal comments (still dummy);
1999-05-24 ago outer syntax keyword classification;