src/HOL/Tools/datatype_rep_proofs.ML
2001-01-16 wenzelm 2001-01-16 proper induction rule for arbitrarily branching datatype;
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-03-15 berghofe 2000-03-15 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-11-11 paulson 1999-11-11 new-style infix declaration for "image"
1999-10-21 wenzelm 1999-10-21 proper handling of axioms / defs;
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