src/HOL/IMP/Collecting.thy
2015-12-19 haftmann 2015-12-19 abandoned attempt to unify sublocale and interpretation into global theories
2015-11-14 haftmann 2015-11-14 coalesce permanent_interpretation.ML with interpretation.ML
2015-09-15 nipkow 2015-09-15 goali -> i
2014-02-19 haftmann 2014-02-19 offical tool
2014-02-19 haftmann 2014-02-19 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
2013-05-17 nipkow 2013-05-17 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
2013-05-16 nipkow 2013-05-16 finally: acom with pointwise access and update of annotations
2013-04-07 nipkow 2013-04-07 cleaned
2013-04-07 nipkow 2013-04-07 cleaned
2013-04-04 nipkow 2013-04-04 tuned
2013-03-11 nipkow 2013-03-11 more factorisation of Step & Co
2013-03-10 nipkow 2013-03-10 factored out Step
2013-02-13 nipkow 2013-02-13 tuned names
2012-09-27 nipkow 2012-09-27 tuned
2012-09-21 nipkow 2012-09-21 conected CS to big-step
2012-09-16 nipkow 2012-09-16 got rid of ad-hoc lift function
2012-09-13 nipkow 2012-09-13 tuned
2012-09-03 nipkow 2012-09-03 added annotations after condition in if and while
2012-08-10 nipkow 2012-08-10 Improved complete lattice formalisation - no more index set.
2012-04-28 nipkow 2012-04-28 renamed Semi to Seq
2012-01-26 nipkow 2012-01-26 tuned
2012-01-04 nipkow 2012-01-04 generalised type
2012-01-02 nipkow 2012-01-02 tuned
2012-01-02 nipkow 2012-01-02 removed unnecessary lemmas
2012-01-01 nipkow 2012-01-01 tuned argument order
2011-12-20 nipkow 2011-12-20 tuned
2011-12-16 nipkow 2011-12-16 improved indexed complete lattice
2011-12-15 nipkow 2011-12-15 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