src/HOL/Tools/recdef_package.ML
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2007-10-09 wenzelm 2007-10-09 Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-18 haftmann 2007-09-18 distinction between regular and default code theorems
2007-08-28 berghofe 2007-08-28 Adapted to changes in interface of Specification.theorem_i
2007-07-29 wenzelm 2007-07-29 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-01-19 wenzelm 2007-01-19 moved parts of OuterParse to SpecParse;
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic; tuned;
2006-11-21 wenzelm 2006-11-21 simplified Proof.theorem(_i);
2006-11-14 wenzelm 2006-11-14 recdef_tc(_i): local_theory interface via Specification.theorem_i; incorporated IsarThy into IsarCmd;
2006-10-23 haftmann 2006-10-23 switched merge_alists'' to AList.merge'' whenever appropriate
2006-10-20 haftmann 2006-10-20 slight cleanup
2006-08-02 wenzelm 2006-08-02 export get_hints; tuned;
2006-06-05 krauss 2006-06-05 HOL/Tools/function_package: Added support for mutual recursive definitions.
2006-05-20 wenzelm 2006-05-20 List.partition;
2006-05-07 wenzelm 2006-05-07 removed 'concl is' patterns;
2006-05-05 krauss 2006-05-05 First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.
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;