src/HOL/Tools/datatype_package.ML
2005-06-11 wenzelm 2005-06-11 refer to name spaces values instead of names;
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src; Args.maybe;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2005-01-18 berghofe 2005-01-18 induct_tac and case_tac no longer depend on Syntax.string_of_vname.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-08 berghofe 2004-06-08 Added exception Datatype_Empty.
2004-05-21 berghofe 2004-05-21 Added more flexible parse / print translations for case expressions.
2004-03-17 berghofe 2004-03-17 case_tac no longer raises THM exception if goal number is out of range.
2004-02-25 berghofe 2004-02-25 find_tname now handles parameter renaming properly ("as they are printed").
2003-08-29 ballarin 2003-08-29 Methods rule_tac etc support static (Isar) contexts.
2002-10-10 berghofe 2002-10-10 Reimplemented parts of datatype package dealing with datatypes involving function types. Now also supports functions with more than one argument.
2002-08-08 wenzelm 2002-08-08 use Tactic.prove instead of prove_goalw_cterm in internal proofs!
2002-08-07 berghofe 2002-08-07 Added calls to add_dt_realizers.
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2002-07-10 berghofe 2002-07-10 Simplified proof of induction rule for datatypes involving function types.
2002-02-21 wenzelm 2002-02-21 clarified internal theory dependencies;
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2002-01-11 wenzelm 2002-01-11 clarified IsarThy.apply_theorems_i;
2001-12-10 berghofe 2001-12-10 Recursive equations to be used for code generation are now registered via RecfunCodegen.add
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-08 wenzelm 2001-11-08 theory data: finish method;
2001-10-27 wenzelm 2001-10-27 Isar: fixed rep_datatype args;
2001-10-16 wenzelm 2001-10-16 declare projected induction rules stemming from nested recursion;
2001-10-12 wenzelm 2001-10-12 HOLogic.dest_concls, InductAttrib.vars_of;
2001-08-31 wenzelm 2001-08-31 tuned headers;
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;