src/HOL/Tools/datatype_prop.ML
2008-05-23 haftmann 2008-05-23 moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
2007-10-23 haftmann 2007-10-23 tuned
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-08-01 wenzelm 2007-08-01 simplified internal Config interface;
2007-07-31 wenzelm 2007-07-31 replaced dtK ref by datatype_distinctness_limit configuration option;
2007-05-17 haftmann 2007-05-17 abstract size function in hologic.ML
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2006-12-01 haftmann 2006-12-01 slight cleanup in hologic.ML
2006-10-20 haftmann 2006-10-20 slight cleanup
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2005-09-20 haftmann 2005-09-20 introduced AList module in favor of assoc etc.
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 Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-21 berghofe 2004-05-21 Added more flexible parse / print translations for case expressions.
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-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2002-08-07 berghofe 2002-08-07 Exported function make_tnames.
2002-07-10 berghofe 2002-07-10 Simplified proof of induction rule for datatypes involving function types.
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-10-27 wenzelm 2001-10-27 hardwire qualified const names;
2001-08-31 wenzelm 2001-08-31 tuned headers;
2001-01-16 wenzelm 2001-01-16 proper induction rule for arbitrarily branching datatype;
2000-10-13 nipkow 2000-10-13 *** empty log message ***
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-08-30 berghofe 2000-08-30 Improved names for size function.
2000-06-13 wenzelm 2000-06-13 rename @case to _case_syntax (improves on low-level errors);
2000-03-28 nipkow 2000-03-28 added weak_case_cong feature
2000-03-13 wenzelm 2000-03-13 use HOLogic.Not; export indexify_names;
1999-10-04 wenzelm 1999-10-04 eliminated ap/app;
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-03-17 wenzelm 1999-03-17 Theory.sign_of;
1998-10-20 wenzelm 1998-10-20 fixed Syntax module;
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-07-24 berghofe 1998-07-24 New datatype definition package