src/HOL/Induct/Com.thy
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