src/HOL/IMP/Abs_Int0.thy
2015-09-15 nipkow 2015-09-15 goali -> i
2015-08-19 paulson 2015-08-19 New material and fixes related to the forthcoming Stone-Weierstrass development
2014-11-09 nipkow 2014-11-09 avoid erule and rotated in IMP
2014-11-08 wenzelm 2014-11-08 avoid slow metis proof;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-01-08 nipkow 2014-01-08 tuned
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-07-03 nipkow 2013-07-03 tuned names
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 tuned
2013-05-16 nipkow 2013-05-16 finally: acom with pointwise access and update of annotations
2013-05-14 nipkow 2013-05-14 tuned names
2013-04-30 nipkow 2013-04-30 canonical names of classes
2013-04-29 nipkow 2013-04-29 tuned
2013-04-26 nipkow 2013-04-26 more standard argument order
2013-04-26 nipkow 2013-04-26 more standard order of arguments
2013-04-26 nipkow 2013-04-26 simplified def
2013-04-24 nipkow 2013-04-24 tuned
2013-04-24 nipkow 2013-04-24 moved defs into locale to reduce unnecessary polymorphism; tuned
2013-04-20 nipkow 2013-04-20 proved termination for fun-based AI
2013-04-20 nipkow 2013-04-20 tuned
2013-04-17 nipkow 2013-04-17 moved leastness lemma
2013-04-11 nipkow 2013-04-11 tuned
2013-04-06 nipkow 2013-04-06 tuned
2013-04-05 nipkow 2013-04-05 tuned document
2013-03-11 nipkow 2013-03-11 more factorisation of Step & Co
2013-03-10 nipkow 2013-03-10 factored out Step
2013-03-06 nipkow 2013-03-06 major redesign: order instead of preorder, new definition of intervals as quotients
2013-02-12 nipkow 2013-02-12 tuned top
2013-01-19 nipkow 2013-01-19 simplified proofs
2013-01-15 nipkow 2013-01-15 tuned
2012-09-21 nipkow 2012-09-21 tuned names
2012-09-20 nipkow 2012-09-20 removed lpfp and proved least pfp thm
2012-09-16 nipkow 2012-09-16 converted wt into a set, tuned names
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-04-19 nipkow 2012-04-19 added revised version of Abs_Int
2012-01-29 nipkow 2012-01-29 removed accidental dependance of abstract interpreter on gamma
2012-01-27 nipkow 2012-01-27 removed duplicate definitions that made locale inconsistent
2012-01-26 nipkow 2012-01-26 tuned
2012-01-18 nipkow 2012-01-18 introduced commands over a set of vars
2012-01-09 nipkow 2012-01-09 Added termination to IMP Abs_Int
2012-01-07 nipkow 2012-01-07 tuned
2012-01-02 nipkow 2012-01-02 tuned
2012-01-02 nipkow 2012-01-02 tuned proofs
2012-01-01 nipkow 2012-01-01 tuned var names
2012-01-01 nipkow 2012-01-01 tuned argument order
2011-12-31 nipkow 2011-12-31 tuned types
2011-12-29 nipkow 2011-12-29 tuned
2011-12-16 nipkow 2011-12-16 improved indexed complete lattice
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
2011-10-12 nipkow 2011-10-12 separated monotonicity reasoning and defined narrowing with while_option
2011-09-28 nipkow 2011-09-28 Added Hoare-like Abstract Interpretation