src/HOL/IMP/Machines.thy
2009-07-27 krauss 2009-07-27 "more standard" argument order of relation composition (op O)
2009-07-09 krauss 2009-07-09 move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure
2009-07-09 krauss 2009-07-09 drop unused lemmas
2009-04-20 haftmann 2009-04-20 power operation on functions with syntax o^; power operation on relations with syntax ^^
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-02-07 berghofe 2007-02-07 Adapted to changes in Transitive_Closure theory.
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2005-12-08 wenzelm 2005-12-08 tuned proofs;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2002-10-24 nipkow 2002-10-24 ASIN -> SET
2002-09-30 berghofe 2002-09-30 Adapted to new simplifier.
2002-04-29 nipkow 2002-04-29 Better compiler proof
2002-04-26 nipkow 2002-04-26 New machine architecture and other direction of compiler proof.