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