src/HOL/Tools/datatype_rep_proofs.ML
1999-10-04 wenzelm 1999-10-04 eliminated ap/app;
1999-09-07 wenzelm 1999-09-07 isatool expandshort;
1999-08-19 berghofe 1999-08-19 Moved sum_case stuff from Sum to Datatype.
1999-08-18 berghofe 1999-08-18 Renamed sum_case to basic_sum_case.
1999-08-17 berghofe 1999-08-17 Tuned some comments.
1999-08-12 berghofe 1999-08-12 Tuned.
1999-07-16 berghofe 1999-07-16 - Datatype package now also supports arbitrarily branching datatypes (using function types). - Added new simplification procedure for proving distinctness of constructors. - dtK is now a reference.
1999-04-27 wenzelm 1999-04-27 adapted add_inductive;
1999-04-14 wenzelm 1999-04-14 tuned messages;
1999-04-14 wenzelm 1999-04-14 intrs: provide names and atts;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-02-03 paulson 1999-02-03 inj is now a translation of inj_on
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-10-20 wenzelm 1998-10-20 quiet proofs;
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-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 Deleted obsolete comments.
1998-07-24 berghofe 1998-07-24 New datatype definition package