src/HOL/Tools/datatype_prop.ML
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-03-10 ago renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2005-09-20 ago introduced AList module in favor of assoc etc.
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 Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
2004-06-21 ago Merged in license change from Isabelle2004
2004-05-21 ago Added more flexible parse / print translations for case expressions.
2002-10-10 ago Reimplemented parts of datatype package dealing with datatypes involving
2002-09-26 ago Converted Fun to Isar style.
2002-08-07 ago Exported function make_tnames.
2002-07-10 ago Simplified proof of induction rule for datatypes involving function types.
2001-12-01 ago renamed class "term" to "type" (actually "HOL.type");
2001-10-27 ago hardwire qualified const names;
2001-08-31 ago tuned headers;
2001-01-16 ago proper induction rule for arbitrarily branching datatype;
2000-10-13 ago *** empty log message ***
2000-10-12 ago *** empty log message ***
2000-08-30 ago Improved names for size function.
2000-06-13 ago rename @case to _case_syntax (improves on low-level errors);
2000-03-28 ago added weak_case_cong feature
2000-03-13 ago use HOLogic.Not;
1999-10-04 ago eliminated ap/app;
1999-07-16 ago - Datatype package now also supports arbitrarily branching datatypes
1999-03-17 ago Theory.sign_of;
1998-10-20 ago fixed Syntax module;
1998-09-26 ago Package now chooses type variable names more carefully to
1998-07-24 ago New datatype definition package