src/HOL/Isar_examples/W_correct.thy
Fri, 28 Sep 2001 19:19:26 +0200 wenzelm inductive: no collective atts;
Mon, 06 Nov 2000 22:56:07 +0100 wenzelm improved: 'induct' handle non-atomic goals;
Fri, 03 Nov 2000 21:33:53 +0100 wenzelm adapted "obtain" proofs;
Tue, 03 Oct 2000 22:36:22 +0200 wenzelm tuned;
Sun, 17 Sep 2000 22:19:02 +0200 wenzelm isar-strip-terminators;
Sat, 19 Aug 2000 12:44:39 +0200 wenzelm tuned;
Thu, 17 Aug 2000 10:34:11 +0200 wenzelm 'symmetric' attribute;
Mon, 14 Aug 2000 18:13:14 +0200 wenzelm intros;
Sun, 30 Jul 2000 13:03:49 +0200 wenzelm adapted obtain;
Thu, 16 Mar 2000 00:36:22 +0100 wenzelm Splitter support;
Mon, 13 Mar 2000 15:42:19 +0100 wenzelm use cases;
Thu, 24 Feb 2000 21:33:32 +0100 wenzelm simplified induct method;
Tue, 22 Feb 2000 21:50:02 +0100 wenzelm tuned "induct" syntax;
Thu, 06 Jan 2000 16:00:18 +0100 wenzelm obtain: renamed 'in' to 'where';
Wed, 05 Jan 2000 12:01:14 +0100 wenzelm obtain;
Sat, 30 Oct 1999 20:20:48 +0200 wenzelm improved presentation;
Thu, 28 Oct 1999 19:57:34 +0200 wenzelm improved presentation;
Fri, 08 Oct 1999 16:47:44 +0200 wenzelm tuned presentation;
Fri, 08 Oct 1999 15:09:14 +0200 wenzelm improved presentation;
Wed, 06 Oct 1999 18:50:51 +0200 wenzelm improved presentation;
Thu, 30 Sep 1999 23:37:22 +0200 wenzelm fixed 'is' match;
Wed, 29 Sep 1999 14:39:35 +0200 wenzelm lemma;
Tue, 28 Sep 1999 14:24:22 +0200 wenzelm added W_correct -- correctness of Milner's type inference algorithm W
less more (0) tip