src/HOL/Tools/recdef_package.ML
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;
1999-05-04 ago add_recdef: removed names / attributes;
1999-04-30 ago peoper defer_recdef interface;
1999-04-27 ago proper quiet_mode;
1999-04-22 ago add_recdef: actual simpset;
1999-04-20 ago temporarily fake quiet_mode;
1999-04-16 ago 'HOL/recdef' theory data;
1999-04-14 ago Wrapper module for Konrad Slind's TFL package.