src/HOL/Recdef.thy
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;