src/HOL/IMP/Compiler0.thy
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
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-05-10 nipkow 2002-05-10 commented out half converted proof
2002-05-07 nipkow 2002-05-07 a bit of conversion to structured proofs
2002-04-26 nipkow 2002-04-26 New machine architecture and other direction of compiler proof.