src/HOL/Tools/primrec_package.ML
2000-11-28 ago RuleCases.save;
2000-08-10 ago Equations that are added to the simpset now have proper names.
2000-07-13 ago adapted PureThy.add_defs_i;
2000-05-25 ago improved error msgs, listing variable names
2000-03-15 ago Added new theory data slot for primrec equations.
2000-03-13 ago adapted to new PureThy.add_thms etc.;
1999-10-21 ago proper handling of axioms / defs;
1999-10-05 ago Got rid of readtm.
1999-09-20 ago Fixed bug in add_primrec which caused non-informative error message.
1999-08-02 ago tuned outer syntax;
1999-07-16 ago - Now also supports arbitrarily branching datatypes.
1999-05-25 ago formal comments (still dummy);
1999-05-24 ago outer syntax keyword classification;
1999-04-14 ago triple_swap;
1999-04-14 ago tuned messages;
1999-04-14 ago tuned comments;
1999-03-17 ago Theory.sign_of;
1999-03-17 ago local open OuterParse;
1999-03-11 ago add_primrec(_i): attributes;
1999-01-12 ago eliminated tthm type and Attribute structure;
1998-12-28 ago better indentation
1998-12-18 ago moved dest_eq to hologic.ML and tidied
1998-11-16 ago Attribute.tthms_of;
1998-10-21 ago Changed interface.
1998-09-24 ago renamed mk_meta_eq to mk_eq
1998-08-12 ago renamed mk_meta_eq to meta_eq
1998-07-30 ago Equations are now stored in theory.
1998-07-24 ago New primrec function definition package