src/HOL/Tools/datatype_package.ML
2005-12-22 wenzelm 2005-12-22 *.inducts holds all projected rules;
2005-12-21 haftmann 2005-12-21 slight improvements
2005-12-21 haftmann 2005-12-21 slight clean ups
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-12-01 berghofe 2005-12-01 Added new component "sorts" to record datatype_info.
2005-12-01 haftmann 2005-12-01 oriented pairs theory * 'a to 'a * theory
2005-10-28 haftmann 2005-10-28 swapped add_datatype result
2005-10-21 wenzelm 2005-10-21 Goal.prove;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-09-20 haftmann 2005-09-20 introduced AList module in favor of assoc etc.
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-08-16 paulson 2005-08-16 classical rules must have names for ATP integration
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-08-01 wenzelm 2005-08-01 simprocs: Simplifier.inherit_bounds;
2005-07-04 haftmann 2005-07-04 (intermediate commit)
2005-07-01 berghofe 2005-07-01 Adapted to new interface of RecfunCodegen.add.
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; Sign.the_const_type; Context.exists_name;
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 ***