src/HOL/Tools/datatype_package.ML
2001-01-18 ago Sign.exists_stamp;
2001-01-16 ago proper induction rule for arbitrarily branching datatype;
2000-11-28 ago RuleCases.save;
2000-10-19 ago InductAttrib;
2000-10-13 ago *** empty log message ***
2000-10-12 ago *** empty log message ***
2000-10-02 ago export get_datatypes_sg;
2000-08-30 ago introduced induct_thm_tac
2000-08-30 ago Improved names for size function.
2000-08-29 ago Simplifier.cong_add_global;
2000-08-28 ago 'induct_tac' / 'case_tac': Method.goal_args';
2000-07-18 ago theorems foo.splits = foo.split foo.split_asm;
2000-06-26 ago export proper induction rule;
2000-04-12 ago InductMethod.concls_of;
2000-04-12 ago improved induct_tac;
2000-04-12 ago fixed 'induct_tac' syntax;
2000-04-05 ago induct/case_tac emulation: optional rule;
2000-03-31 ago use cong_add_global att;
2000-03-28 ago added weak_case_cong feature
2000-03-20 ago proof methods: 'case_tac' / 'induct_tac';
2000-03-15 ago Eliminated store_clasimp.
2000-03-13 ago case_tac now subsumes both boolean and datatype cases;
2000-03-13 ago removed cases_of;
2000-03-10 ago add_cases_induct: produce proper case names;
2000-03-01 ago project induct rule;
2000-02-27 ago HOLogic.dest_conj;
2000-02-22 ago added cases_tac;
2000-01-05 ago replaced HOLogic.termTVar by HOLogic.termT;
1999-10-21 ago proper handling of axioms / defs;
1999-10-13 ago Eliminated mutual_induct_tac.
1999-10-05 ago rep_datatype now stores theorems properly.
1999-08-02 ago handle LIST _;
1999-07-22 ago Tuned.
1999-07-20 ago Eliminated addDistinct.
1999-07-16 ago - Datatype package now also supports arbitrarily branching datatypes
1999-06-28 ago cond_extern_table;
1999-06-04 ago no message "Adding axioms for datatype(s)";
1999-05-25 ago formal comments (still dummy);
1999-05-24 ago outer syntax keyword classification;
1999-04-30 ago theory data: copy;
1999-04-22 ago rep_datatype syntax: 'induction' instead of 'induct';
1999-04-16 ago print_datatypes;
1999-04-14 ago tuned messages;
1999-04-14 ago tuned comments;
1999-03-17 ago Theory.sign_of;
1999-03-17 ago rep_datatype: '_i' version, attributes, outer syntax;
1999-03-11 ago outer syntax for 'datatype';
1999-03-05 ago Fixed bug in add_datatype_axm:
1999-01-12 ago get_tthms witness theorems;
1999-01-12 ago eliminated tthm type and Attribute structure;
1998-11-16 ago Attribute.tthms_of;
1998-10-21 ago Changed interface of rep_datatype: Characteristic theorems
1998-10-16 ago Fixed bug (improper handling of flag flat_names).
1998-10-16 ago - Changed structure of name spaces
1998-09-26 ago Package now chooses type variable names more carefully to
1998-08-06 ago Improved well-formedness check.
1998-07-24 ago New datatype definition package