src/HOL/Induct/Com.thy
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-06-20 wenzelm 2015-06-20 isabelle update_cartouches;
2015-03-25 wenzelm 2015-03-25 prefer local fixes;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-11 blanchet 2014-09-11 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
2011-09-18 wenzelm 2011-09-18 tuned proofs;
2011-08-12 huffman 2011-08-12 make more HOL theories work with separate set type
2011-02-22 wenzelm 2011-02-22 modernized specifications;
2010-05-12 wenzelm 2010-05-12 removed obsolete CVS Ids;
2009-08-13 paulson 2009-08-13 Removal of redundant settings of unification trace and search bounds.
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2007-10-03 wenzelm 2007-10-03 avoid unnamed infixes;
2007-08-07 wenzelm 2007-08-07 turned Unify flags into configuration options (global only);
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2006-05-27 wenzelm 2006-05-27 tuned;
2005-11-25 wenzelm 2005-11-25 tuned induct proofs;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-04-07 paulson 2004-04-07 IsaMakefile
2002-04-02 paulson 2002-04-02 conversion of some HOL/Induct proof scripts to Isar
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-08-06 nipkow 2001-08-06 turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'.
2001-01-02 nipkow 2001-01-02 *** empty log message ***
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-06-30 berghofe 1998-06-30 Adapted to new inductive definition package.
1997-11-21 oheimb 1997-11-21 minor improvements of formulation and proofs
1997-05-09 paulson 1997-05-09 Fixed precedence of semicolon
1997-05-07 paulson 1997-05-07 New directory to contain examples of (co)inductive definitions