src/HOL/Recdef.thy
2009-08-31 krauss 2009-08-31 moved wfrec to Recdef.thy
2009-07-28 krauss 2009-07-28 moved obsolete same_fst to Recdef.thy
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-01-28 haftmann 2009-01-28 Plain, Main form meeting points in import hierarchy
2008-04-25 krauss 2008-04-25 Merged theories about wellfoundedness into one: Wellfounded.thy
2007-07-11 berghofe 2007-07-11 Removed wf_implies_wfP and wfP_implies_wf from list of hints again.
2007-05-31 wenzelm 2007-05-31 moved TFL files to canonical place;
2007-04-10 krauss 2007-04-10 Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
2007-03-03 haftmann 2007-03-03 moved instance option :: finite to Finite_Set.thy
2007-02-07 berghofe 2007-02-07 Theorems for converting between wf and wfP are now declared as hints.
2006-06-05 krauss 2006-06-05 HOL/Tools/function_package: Added support for mutual recursive definitions.
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.
2005-12-02 krauss 2005-12-02 Added recdef congruence rules for bounded quantifiers and commonly used higher order functions.
2005-08-09 nipkow 2005-08-09 added finite(option) to Recdef.thy
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-08-20 paulson 2004-08-20 fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2001-12-10 berghofe 2001-12-10 Moved code generator setup from Recdef to Inductive.
2001-11-03 wenzelm 2001-11-03 tuned;
2001-08-31 berghofe 2001-08-31 Added code generator setup.
2001-07-25 paulson 2001-07-25 Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
2001-05-04 nipkow 2001-05-04 made same_fst recdef_simp
2001-02-20 oheimb 2001-02-20 added image_cong to default congs of recdef
2001-01-03 wenzelm 2001-01-03 renamed .sml files to .ML; tuned package setup;
2000-12-13 nipkow 2000-12-13 small mods.
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-09-05 wenzelm 2000-09-05 improved recdef setup;
2000-02-27 wenzelm 2000-02-27 early setup of induct_method;
1999-10-04 wenzelm 1999-10-04 load / setup recdef package (TFL);
1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;
1999-04-16 wenzelm 1999-04-16 'HOL/recdef' theory data; induct method setup;
1998-07-03 wenzelm 1998-07-03 stepping stones;