src/HOL/Library/While_Combinator.thy
Thu, 18 Dec 2003 08:20:36 +0100 nipkow *** empty log message ***
Thu, 17 Jan 2002 15:06:36 +0100 kleing registered directly executable version with the code generator
Tue, 23 Oct 2001 22:58:15 +0200 wenzelm eliminated old numerals;
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,
Fri, 28 Sep 2001 19:17:01 +0200 wenzelm recdef (permissive);
Tue, 04 Sep 2001 21:10:57 +0200 wenzelm renamed "antecedent" case to "rule_context";
Fri, 04 May 2001 15:38:48 +0200 nipkow made same_fst recdef_simp
Sat, 03 Feb 2001 17:43:05 +0100 wenzelm tuned;
Mon, 29 Jan 2001 23:54:56 +0100 wenzelm avoid dead code;
Fri, 26 Jan 2001 15:50:52 +0100 nipkow Merged Example into While_Combi
Wed, 03 Jan 2001 21:24:29 +0100 wenzelm recdef_tc;
Thu, 14 Dec 2000 19:37:27 +0100 wenzelm unsymbolize;
Wed, 13 Dec 2000 09:32:55 +0100 nipkow small mods.
Thu, 19 Oct 2000 01:48:26 +0200 wenzelm use RecdefPackage.tcs_of;
Wed, 18 Oct 2000 23:29:49 +0200 wenzelm A general ``while'' combinator (from main HOL);
less more (0) tip