src/HOL/Induct/Com.thy
Thu, 13 Aug 2009 17:19:42 +0100 paulson Removal of redundant settings of unification trace and search bounds.
Wed, 07 May 2008 10:57:19 +0200 berghofe Adapted to encoding of sets as predicates
Wed, 03 Oct 2007 19:49:33 +0200 wenzelm avoid unnamed infixes;
Tue, 07 Aug 2007 20:19:55 +0200 wenzelm turned Unify flags into configuration options (global only);
Wed, 11 Jul 2007 11:14:51 +0200 berghofe Adapted to new inductive definition package.
Sat, 27 May 2006 17:42:02 +0200 wenzelm tuned;
Fri, 25 Nov 2005 21:14:34 +0100 wenzelm tuned induct proofs;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Wed, 07 Apr 2004 14:25:48 +0200 paulson IsaMakefile
Tue, 02 Apr 2002 14:28:28 +0200 paulson conversion of some HOL/Induct proof scripts to Isar
Sat, 01 Dec 2001 18:52:32 +0100 wenzelm renamed class "term" to "type" (actually "HOL.type");
Fri, 05 Oct 2001 21:52:39 +0200 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
Mon, 06 Aug 2001 13:43:24 +0200 nipkow turned translation for 1::nat into def.
Tue, 02 Jan 2001 10:27:10 +0100 nipkow *** empty log message ***
Fri, 24 Jul 1998 13:19:38 +0200 berghofe Adapted to new datatype package.
less more (0) -15 tip