src/HOL/Isar_examples/Fibonacci.thy
Mon, 22 Jun 2009 23:48:24 +0200 wenzelm observe standard theory naming conventions;
Mon, 14 Jul 2008 11:04:42 +0200 haftmann unified curried gcd, lcm, zgcd, zlcm
Thu, 26 Jun 2008 10:06:53 +0200 haftmann dropped recdef
Wed, 23 Nov 2005 22:26:13 +0100 wenzelm tuned induction proofs;
Thu, 10 Nov 2005 21:14:05 +0100 wenzelm tuned proofs;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Fri, 14 Jan 2005 12:00:27 +0100 nipkow made diff_less a simp rule
Tue, 16 Oct 2001 17:58:13 +0200 wenzelm tuned induction proofs;
Sat, 06 Oct 2001 00:02:46 +0200 wenzelm * sane numerals (stage 2): plain "num" syntax (removed "#");
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.
Mon, 06 Nov 2000 22:56:07 +0100 wenzelm improved: 'induct' handle non-atomic goals;
Sun, 17 Sep 2000 22:19:02 +0200 wenzelm isar-strip-terminators;
Wed, 06 Sep 2000 08:04:41 +0200 nipkow less_induct -> nat_less_induct
Mon, 04 Sep 2000 10:26:34 +0200 paulson minor fixes for new version of Primes.thy
Sat, 19 Aug 2000 12:44:39 +0200 wenzelm tuned;
Tue, 23 May 2000 18:06:22 +0200 paulson added type constraint ::nat because 0 is now overloaded
Fri, 05 May 2000 22:30:14 +0200 wenzelm adapted to new arithmetic simprocs;
Thu, 30 Mar 2000 19:45:51 +0200 nipkow recdef.rules -> recdef.simps
Sun, 27 Feb 2000 15:25:31 +0100 wenzelm even better induct setup;
Tue, 22 Feb 2000 21:50:02 +0100 wenzelm tuned "induct" syntax;
Tue, 07 Dec 1999 17:14:49 +0100 wenzelm tuned;
Tue, 07 Dec 1999 12:13:09 +0100 wenzelm tuned;
less more (0) tip