src/HOL/Tools/recdef_package.ML
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;
2001-01-03 wenzelm 2001-01-03 added recdef_tc(_i);
2000-10-19 wenzelm 2000-10-19 added tcs_of;
2000-09-19 wenzelm 2000-09-19 tuned;
2000-09-15 wenzelm 2000-09-15 added "congs" keyword;
2000-09-15 wenzelm 2000-09-15 "hints" made keyword again;
2000-09-13 wenzelm 2000-09-13 tuned recdef hints;
2000-09-07 wenzelm 2000-09-07 tuned msg;
2000-09-06 wenzelm 2000-09-06 make SML/NJ happy;
2000-09-06 wenzelm 2000-09-06 tuned;
2000-09-05 wenzelm 2000-09-05 recdef hints (attributes and modifiers);
2000-08-18 wenzelm 2000-08-18 removed obsolete add_recdef_x;
2000-08-17 nipkow 2000-08-17 installed recdef congs data
2000-04-18 wenzelm 2000-04-18 removed obsolete "simpset" keyword;
2000-04-13 wenzelm 2000-04-13 outer syntax: no simps;
2000-04-01 wenzelm 2000-04-01 recdef: admit names/atts;
2000-03-30 nipkow 2000-03-30 If all termination conditions are proved automatically, the recusrion equations are added to the simpset automatically. recdef.rules -> recdef.simps
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.