src/HOL/IMP/Comp_Rev.thy
Thu, 28 Jul 2011 15:15:26 +0200 resolved code_pred FIXME in IMP; clearer notation for exec_n
Fri, 17 Jun 2011 20:38:43 +0200 IMP compiler with int, added reverse soundness direction