src/HOL/Tools/datatype_abs_proofs.ML
2001-01-16 ago proper induction rule for arbitrarily branching datatype;
2000-10-13 ago *** empty log message ***
2000-10-12 ago *** empty log message ***
2000-09-15 ago renamed (most of...) the select rules
2000-08-30 ago Improved names for size function.
2000-07-13 ago adapted PureThy.add_defs_i;
2000-03-28 ago added weak_case_cong feature
2000-03-15 ago - Fixed bug in prove_casedist_thms (proof failed because of
2000-03-13 ago adapted to new PureThy.add_thms etc.;
2000-02-27 ago HOLogic.dest_conj;
1999-10-21 ago proper handling of axioms / defs;
1999-10-04 ago eliminated ap/app;
1999-08-17 ago Tuned some comments.
1999-07-16 ago - Datatype package now also supports arbitrarily branching datatypes
1999-04-27 ago adapted add_inductive;
1999-04-14 ago tuned messages;
1999-04-14 ago intrs: provide names and atts;
1999-03-17 ago Theory.sign_of;
1999-01-12 ago eliminated tthm type and Attribute structure;
1998-11-16 ago Attribute.tthms_of;
1998-10-16 ago - Changed structure of name spaces
1998-09-26 ago Package now chooses type variable names more carefully to
1998-09-24 ago renamed mk_meta_eq to mk_eq
1998-08-12 ago renamed mk_meta_eq to meta_eq
1998-07-24 ago New datatype definition package