src/HOL/Tools/datatype_abs_proofs.ML
2000-03-15 berghofe 2000-03-15 - Fixed bug in prove_casedist_thms (proof failed because of name clashes) - Now returns theorems with correct names in derivations
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.; proper handling of case names;
2000-02-27 wenzelm 2000-02-27 HOLogic.dest_conj;
1999-10-21 wenzelm 1999-10-21 proper handling of axioms / defs;
1999-10-04 wenzelm 1999-10-04 eliminated ap/app;
1999-08-17 berghofe 1999-08-17 Tuned some comments.
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-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-11-16 wenzelm 1998-11-16 Attribute.tthms_of;
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-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-24 berghofe 1998-07-24 New datatype definition package