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