src/HOL/Induct/Term.thy
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 ported Induct to new datatypes
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2012-03-14 wenzelm 2012-03-14 misc tuning;
2010-06-28 haftmann 2010-06-28 modernized specifications
2010-05-12 wenzelm 2010-05-12 removed obsolete CVS Ids;
2005-12-22 wenzelm 2005-12-22 tuned;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2002-02-25 wenzelm 2002-02-25 clarified syntax of ``long'' statements: fixes/assumes/shows;
2001-11-13 wenzelm 2001-11-13 tuned inductions;
2001-10-16 wenzelm 2001-10-16 tuned induction proofs;
2001-10-01 wenzelm 2001-10-01 tuned;
2001-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
2001-02-03 wenzelm 2001-02-03 Induct: converted some theories to new-style format;
1998-10-23 berghofe 1998-10-23 Terms are now defined using the new datatype package.
1998-10-21 berghofe 1998-10-21 Changed syntax of inductive.
1998-07-24 berghofe 1998-07-24 Renamed '$' to 'Scons' because of clashes with constants of the same name in theories using datatypes.
1997-05-07 paulson 1997-05-07 New directory to contain examples of (co)inductive definitions