src/HOL/Tools/datatype_package.ML
2001-05-31 oheimb 2001-05-31 improved iff_add_global, new function add_rules factoring out common behaviour
2001-01-18 wenzelm 2001-01-18 Sign.exists_stamp;
2001-01-16 wenzelm 2001-01-16 proper induction rule for arbitrarily branching datatype;
2000-11-28 wenzelm 2000-11-28 RuleCases.save;
2000-10-19 wenzelm 2000-10-19 InductAttrib;
2000-10-13 nipkow 2000-10-13 *** empty log message ***
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-10-02 wenzelm 2000-10-02 export get_datatypes_sg; added weak_case_congs_of(_sg);
2000-08-30 nipkow 2000-08-30 introduced induct_thm_tac
2000-08-30 berghofe 2000-08-30 Improved names for size function.
2000-08-29 wenzelm 2000-08-29 Simplifier.cong_add_global;
2000-08-28 wenzelm 2000-08-28 'induct_tac' / 'case_tac': Method.goal_args';
2000-07-18 wenzelm 2000-07-18 theorems foo.splits = foo.split foo.split_asm;
2000-06-26 wenzelm 2000-06-26 export proper induction rule;
2000-04-12 wenzelm 2000-04-12 InductMethod.concls_of;
2000-04-12 wenzelm 2000-04-12 improved induct_tac;
2000-04-12 wenzelm 2000-04-12 fixed 'induct_tac' syntax;
2000-04-05 wenzelm 2000-04-05 induct/case_tac emulation: optional rule; add_cases_induct: fixed case names;
2000-03-31 wenzelm 2000-03-31 use cong_add_global att;
2000-03-28 nipkow 2000-03-28 added weak_case_cong feature
2000-03-20 wenzelm 2000-03-20 proof methods: 'case_tac' / 'induct_tac';
2000-03-15 berghofe 2000-03-15 Eliminated store_clasimp.
2000-03-13 wenzelm 2000-03-13 case_tac now subsumes both boolean and datatype cases;
2000-03-13 wenzelm 2000-03-13 removed cases_of; renamed cases_tac to case_tac; tuned to work with basic HOL as well; add_cases_induct: proper case names; adapted to new PureThy.add_thms etc.;
2000-03-10 wenzelm 2000-03-10 add_cases_induct: produce proper case names;
2000-03-01 wenzelm 2000-03-01 project induct rule;
2000-02-27 wenzelm 2000-02-27 HOLogic.dest_conj; add_cases_induct: induct_method setup;
2000-02-22 wenzelm 2000-02-22 added cases_tac;
2000-01-05 wenzelm 2000-01-05 replaced HOLogic.termTVar by HOLogic.termT;
1999-10-21 wenzelm 1999-10-21 proper handling of axioms / defs;
1999-10-13 berghofe 1999-10-13 Eliminated mutual_induct_tac.
1999-10-05 berghofe 1999-10-05 rep_datatype now stores theorems properly.
1999-08-02 wenzelm 1999-08-02 handle LIST _;
1999-07-22 berghofe 1999-07-22 Tuned.
1999-07-20 berghofe 1999-07-20 Eliminated addDistinct.
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-06-28 wenzelm 1999-06-28 cond_extern_table;
1999-06-04 wenzelm 1999-06-04 no message "Adding axioms for datatype(s)";
1999-05-25 wenzelm 1999-05-25 formal comments (still dummy);
1999-05-24 wenzelm 1999-05-24 outer syntax keyword classification; no open OuterParse;
1999-04-30 wenzelm 1999-04-30 theory data: copy;
1999-04-22 wenzelm 1999-04-22 rep_datatype syntax: 'induction' instead of 'induct';
1999-04-16 wenzelm 1999-04-16 print_datatypes;
1999-04-14 wenzelm 1999-04-14 tuned messages;
1999-04-14 wenzelm 1999-04-14 tuned comments;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-17 wenzelm 1999-03-17 rep_datatype: '_i' version, attributes, outer syntax;
1999-03-11 wenzelm 1999-03-11 outer syntax for 'datatype';
1999-03-05 berghofe 1999-03-05 Fixed bug in add_datatype_axm: Recursion and case combinators were assigned inconsistent names in quick_and_dirty mode, which caused recdef etc. to crash.
1999-01-12 wenzelm 1999-01-12 get_tthms witness theorems;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-11-16 wenzelm 1998-11-16 Attribute.tthms_of; Theory.copy;
1998-10-21 berghofe 1998-10-21 Changed interface of rep_datatype: Characteristic theorems of datatypes are now specified by xstrings.
1998-10-16 berghofe 1998-10-16 Fixed bug (improper handling of flag flat_names).
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-08-06 berghofe 1998-08-06 Improved well-formedness check.
1998-07-24 berghofe 1998-07-24 New datatype definition package