src/HOL/IMP/Live.thy
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-05-17 nipkow 2013-05-17 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
2013-05-14 nipkow 2013-05-14 tuned names
2013-03-21 nipkow 2013-03-21 proofs depend only on constraints, not on def of L WHILE
2013-03-18 nipkow 2013-03-18 tuned
2013-03-15 nipkow 2013-03-15 tuned
2013-03-14 nipkow 2013-03-14 tuned
2013-03-12 nipkow 2013-03-12 added latex markup
2012-11-05 nipkow 2012-11-05 tuned
2012-04-28 nipkow 2012-04-28 renamed Semi to Seq
2011-12-08 nipkow 2011-12-08 tuned
2011-12-06 nipkow 2011-12-06 added lemmas
2011-12-05 nipkow 2011-12-05 tuned proof
2011-10-20 nipkow 2011-10-20 renamed name -> vname
2011-09-20 nipkow 2011-09-20 Updated IMP to use new induction method
2011-09-14 nipkow 2011-09-14 cleand up AbsInt fixpoint iteration; tuned syntax
2011-06-06 kleing 2011-06-06 imported rest of new IMP
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-03-15 nipkow 2010-03-15 tuned inductions
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2008-11-20 nipkow 2008-11-20 added optimizer
2008-10-14 nipkow 2008-10-14 Added liveness analysis