src/HOL/IMP/AExp.thy
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2013-11-07 kleing 2013-11-07 Add output translation for <a := .., b := .., ..> state notation.
2013-11-05 kleing 2013-11-05 use int example like in the rest of IMP (instead of nat)
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-06-27 nipkow 2013-06-27 tuned
2013-02-13 nipkow 2013-02-13 tuned state display
2012-09-07 nipkow 2012-09-07 tuned latex
2011-10-23 nipkow 2011-10-23 tuned
2011-10-22 nipkow 2011-10-22 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
2011-10-21 nipkow 2011-10-21 tuned
2011-10-20 nipkow 2011-10-20 tuned
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-08-04 kleing 2011-08-04 new state syntax with less conflicts
2011-06-07 kleing 2011-06-07 use null_heap instead of %_. 0 to avoid printing problems
2011-06-06 kleing 2011-06-06 imported rest of new IMP
2011-06-01 nipkow 2011-06-01 Replacing old IMP with new Semantics material