src/HOL/Tools/primrec_package.ML
2000-05-25 paulson 2000-05-25 improved error msgs, listing variable names
2000-03-15 berghofe 2000-03-15 Added new theory data slot for primrec equations.
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.; prepare induct rule (case names);
1999-10-21 wenzelm 1999-10-21 proper handling of axioms / defs;
1999-10-05 berghofe 1999-10-05 Got rid of readtm.
1999-09-20 berghofe 1999-09-20 Fixed bug in add_primrec which caused non-informative error message.
1999-08-02 wenzelm 1999-08-02 tuned outer syntax;
1999-07-16 berghofe 1999-07-16 - Now also supports arbitrarily branching datatypes. - Fixed bug (in some rare cases, recursive constants were inconsistently typed in different primrec equations).
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-04-14 wenzelm 1999-04-14 triple_swap;
1999-04-14 wenzelm 1999-04-14 tuned messages;
1999-04-14 wenzelm 1999-04-14 tuned comments; tuned types;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-17 wenzelm 1999-03-17 local open OuterParse;
1999-03-11 wenzelm 1999-03-11 add_primrec(_i): attributes; outer syntax for 'primrec';
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-12-28 paulson 1998-12-28 better indentation
1998-12-18 paulson 1998-12-18 moved dest_eq to hologic.ML and tidied
1998-11-16 wenzelm 1998-11-16 Attribute.tthms_of;
1998-10-21 berghofe 1998-10-21 Changed interface.
1998-09-24 oheimb 1998-09-24 renamed mk_meta_eq to mk_eq
1998-08-12 oheimb 1998-08-12 renamed mk_meta_eq to meta_eq
1998-07-30 berghofe 1998-07-30 Equations are now stored in theory.
1998-07-24 berghofe 1998-07-24 New primrec function definition package