src/HOL/Library/While_Combinator.thy
2007-04-26 ago slightly tuned
2006-11-17 ago more robust syntax for definition/abbreviation/notation;
2006-10-01 ago tuned;
2006-06-05 ago Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
2006-05-27 ago tuned;
2005-12-08 ago tuned proofs;
2004-09-10 ago Added antisymmetry simproc
2004-08-18 ago import -> imports
2004-08-16 ago New theory header syntax.
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);