src/HOL/Tools/datatype_package.ML
1999-04-30 wenzelm 1999-04-30 theory data: copy;
1999-04-22 wenzelm 1999-04-22 rep_datatype syntax: 'induction' instead of 'induct';
1999-04-16 wenzelm 1999-04-16 print_datatypes;
1999-04-14 wenzelm 1999-04-14 tuned messages;
1999-04-14 wenzelm 1999-04-14 tuned comments;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-17 wenzelm 1999-03-17 rep_datatype: '_i' version, attributes, outer syntax;
1999-03-11 wenzelm 1999-03-11 outer syntax for 'datatype';
1999-03-05 berghofe 1999-03-05 Fixed bug in add_datatype_axm: Recursion and case combinators were assigned inconsistent names in quick_and_dirty mode, which caused recdef etc. to crash.
1999-01-12 wenzelm 1999-01-12 get_tthms witness theorems;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-11-16 wenzelm 1998-11-16 Attribute.tthms_of; Theory.copy;
1998-10-21 berghofe 1998-10-21 Changed interface of rep_datatype: Characteristic theorems of datatypes are now specified by xstrings.
1998-10-16 berghofe 1998-10-16 Fixed bug (improper handling of flag flat_names).
1998-10-16 berghofe 1998-10-16 - Changed structure of name spaces - Proofs for datatypes with unneeded parameters are working now - added additional parameter flat_names - added quiet_mode flag
1998-09-26 berghofe 1998-09-26 Package now chooses type variable names more carefully to avoid clashes with user-supplied type variable names.
1998-08-06 berghofe 1998-08-06 Improved well-formedness check.
1998-07-24 berghofe 1998-07-24 New datatype definition package