src/HOL/Library/While_Combinator.thy
2004-05-06 ago tuned document;
2004-04-16 ago tuned document;
2003-12-18 ago *** empty log message ***
2002-01-17 ago registered directly executable version with the code generator
2001-10-23 ago eliminated old numerals;
2001-10-06 ago * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 ago sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
2001-09-28 ago recdef (permissive);
2001-09-04 ago renamed "antecedent" case to "rule_context";
2001-05-04 ago made same_fst recdef_simp
2001-02-03 ago tuned;
2001-01-29 ago avoid dead code;
2001-01-26 ago Merged Example into While_Combi
2001-01-03 ago recdef_tc;
2000-12-14 ago unsymbolize;
2000-12-13 ago small mods.
2000-10-19 ago use RecdefPackage.tcs_of;
2000-10-18 ago A general ``while'' combinator (from main HOL);