src/HOL/IMP/Hoare_Examples.thy
2015-08-27 blanchet 2015-08-27 fixed typo in comment
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-07-08 nipkow 2013-07-08 tuned proofs
2013-07-05 nipkow 2013-07-05 improved proof automation for numerals
2013-05-26 nipkow 2013-05-26 simpler proof through custom summation function
2013-05-22 nipkow 2013-05-22 simplified example and proof
2013-05-17 nipkow 2013-05-17 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
2013-01-19 nipkow 2013-01-19 simplified proofs
2012-04-28 nipkow 2012-04-28 renamed Semi to Seq
2011-09-20 nipkow 2011-09-20 Updated IMP to use new induction method
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-13 kleing 2011-08-13 IMP/Util distinguishes between sets and functions again; imported only where used.
2011-06-06 kleing 2011-06-06 imported rest of new IMP