src/HOL/IMP/Compiler.thy
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 ***