src/HOL/Tools/recdef_package.ML
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
1999-06-28 wenzelm 1999-06-28 cond_extern_table;
1999-05-25 wenzelm 1999-05-25 formal comments (still dummy);
1999-05-24 wenzelm 1999-05-24 outer syntax keyword classification; no open OuterParse;
1999-05-04 wenzelm 1999-05-04 add_recdef: removed names / attributes;
1999-04-30 wenzelm 1999-04-30 peoper defer_recdef interface;
1999-04-27 wenzelm 1999-04-27 proper quiet_mode;
1999-04-22 wenzelm 1999-04-22 add_recdef: actual simpset; add_recdef_x: named simpset;
1999-04-20 wenzelm 1999-04-20 temporarily fake quiet_mode;
1999-04-16 wenzelm 1999-04-16 'HOL/recdef' theory data;
1999-04-14 wenzelm 1999-04-14 Wrapper module for Konrad Slind's TFL package.