src/HOL/IMP/Compiler.thy
2011-10-19 nipkow 2011-10-19 renamed B to Bc
2011-10-12 wenzelm 2011-10-12 tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
2011-09-29 Jean Pichon 2011-09-29 fixed typos in IMP
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-04 kleing 2011-08-04 new state syntax with less conflicts
2011-07-28 kleing 2011-07-28 compiler proof cleanup
2011-07-28 kleing 2011-07-28 resolved code_pred FIXME in IMP; clearer notation for exec_n
2011-06-17 kleing 2011-06-17 IMP compiler with int, added reverse soundness direction
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
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-07-09 krauss 2009-07-09 drop unused lemmas
2008-06-25 wenzelm 2008-06-25 modernized specifications;
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2002-10-24 nipkow 2002-10-24 ASIN -> SET
2002-10-08 nipkow 2002-10-08 Got rid of rotates because of new simplifier
2002-04-26 nipkow 2002-04-26 New machine architecture and other direction of compiler proof.
2001-12-20 nipkow 2001-12-20 renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
2001-12-19 wenzelm 2001-12-19 tuned;
2001-12-09 kleing 2001-12-09 tuned for latex output
2001-11-23 nipkow 2001-11-23 Isar conversion
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-04-30 nipkow 2001-04-30 new proof
2000-11-10 nipkow 2000-11-10 JMB -> JMPB. Email von Johannes Pfeifroth.
2000-10-26 nipkow 2000-10-26 *** empty log message ***
2000-10-26 nipkow 2000-10-26 *** empty log message ***