src/HOL/IMP/Collecting1.thy
2013-05-16 nipkow 2013-05-16 finally: acom with pointwise access and update of annotations
2012-01-26 nipkow 2012-01-26 tuned
2012-01-02 nipkow 2012-01-02 tuned
2011-11-27 nipkow 2011-11-27 simplified Collecting1 and renamed: step -> step', step_cs -> step
2011-11-24 nipkow 2011-11-24 Abstract interpretation is now based uniformly on annotated programs, including a collecting and a small step semantics