src/HOL/Tools/datatype_package.ML
2006-01-19 ago setup: theory -> theory;
2006-01-17 ago substantial improvements in code generator
2006-01-15 ago classical attributes: optional weight;
2006-01-14 ago generic attributes;
2006-01-14 ago sane ERROR handling;
2006-01-10 ago generic attributes;
2006-01-09 ago _E suffix for compatibility with AddIffs
2005-12-29 ago adaptions to changes in code generator
2005-12-22 ago *.inducts holds all projected rules;
2005-12-21 ago slight improvements
2005-12-21 ago slight clean ups
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 ago oriented result pairs in PureThy
2005-12-01 ago Added new component "sorts" to record datatype_info.
2005-12-01 ago oriented pairs theory * 'a to 'a * theory
2005-10-28 ago swapped add_datatype result
2005-10-21 ago Goal.prove;
2005-10-17 ago change_claset/simpset;
2005-09-20 ago introduced AList module in favor of assoc etc.
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-12 ago introduced new-style AList operations
2005-09-05 ago curried_lookup/update;
2005-08-16 ago classical rules must have names for ATP integration
2005-08-16 ago OuterKeyword;
2005-08-01 ago simprocs: Simplifier.inherit_bounds;
2005-07-04 ago (intermediate commit)
2005-07-01 ago Adapted to new interface of RecfunCodegen.add.
2005-06-20 ago get_thm(s): Name;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-06-11 ago refer to name spaces values instead of names;
2005-05-31 ago renamed cond_extern to extern;
2005-04-13 ago *** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13 ago *** empty log message ***
2005-04-07 ago reverted renaming of Some/None in comments and strings;
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-01-24 ago Adapted to modified interface of PureThy.get_thm(s).
2005-01-18 ago induct_tac and case_tac no longer depend on Syntax.string_of_vname.
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-08 ago Added exception Datatype_Empty.
2004-05-21 ago Added more flexible parse / print translations for case expressions.
2004-03-17 ago case_tac no longer raises THM exception if goal number is out of range.
2004-02-25 ago find_tname now handles parameter renaming properly ("as they are printed").
2003-08-29 ago Methods rule_tac etc support static (Isar) contexts.
2002-10-10 ago Reimplemented parts of datatype package dealing with datatypes involving
2002-08-08 ago use Tactic.prove instead of prove_goalw_cterm in internal proofs!
2002-08-07 ago Added calls to add_dt_realizers.
2002-08-06 ago sane interface for simprocs;
2002-07-10 ago Simplified proof of induction rule for datatypes involving function types.
2002-02-21 ago clarified internal theory dependencies;
2002-02-12 ago got rid of explicit marginal comments (now stripped earlier from input);
2002-01-11 ago clarified IsarThy.apply_theorems_i;
2001-12-10 ago Recursive equations to be used for code generation are now registered
2001-12-01 ago renamed class "term" to "type" (actually "HOL.type");
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-08 ago theory data: finish method;
2001-10-27 ago Isar: fixed rep_datatype args;
2001-10-16 ago declare projected induction rules stemming from nested recursion;
2001-10-12 ago HOLogic.dest_concls, InductAttrib.vars_of;