src/HOL/Library/While_Combinator.thy
2015-09-13 wenzelm 2015-09-13 renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-09-04 wenzelm 2015-09-04 modernized name space management -- more uniform qualification;
2015-06-25 wenzelm 2015-06-25 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-02-14 blanchet 2014-02-14 merged 'Option.map' and 'Option.map_option'
2013-10-24 traytel 2013-10-24 refactored rtrancl_while; prove termination for finite rtrancl
2013-10-03 nipkow 2013-10-03 added and generalised lemmas
2013-10-02 nipkow 2013-10-02 tuned
2013-09-03 wenzelm 2013-09-03 tuned proofs -- less guessing;
2013-08-28 nipkow 2013-08-28 tuned
2013-08-28 nipkow 2013-08-28 added rtrancl_while
2012-12-17 traytel 2012-12-17 useful commutative diagram for while_option
2012-11-23 nipkow 2012-11-23 moved lemma
2012-11-04 nipkow 2012-11-04 code for while directly, not via while_option
2012-01-30 blanchet 2012-01-30 rename lambda translation schemes
2011-12-13 nipkow 2011-12-13 connect while_option with lfp
2011-02-14 nipkow 2011-02-14 generalized termination lemmas
2011-02-08 nipkow 2011-02-08 added termination lemmas
2010-07-09 krauss 2010-07-09 moved example to its own file in HOL/ex
2010-07-09 krauss 2010-07-09 added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
2009-03-27 haftmann 2009-03-27 normalized imports
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2007-07-16 krauss 2007-07-16 use function package
2007-04-26 haftmann 2007-04-26 slightly tuned
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-10-01 wenzelm 2006-10-01 tuned;
2006-06-05 krauss 2006-06-05 Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". This simplifies some proofs.
2006-05-27 wenzelm 2006-05-27 tuned;
2005-12-08 wenzelm 2005-12-08 tuned proofs;
2004-09-10 nipkow 2004-09-10 Added antisymmetry simproc
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
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);