src/HOL/IMP/Comp_Rev.thy
Sun, 14 Apr 2013 21:54:45 +1000 added another definition snipped
Sun, 24 Feb 2013 13:46:14 +1100 eliminated isize in favour of size + type coercion
Wed, 14 Nov 2012 14:45:14 +0100 tuned text
Wed, 14 Nov 2012 14:11:47 +0100 replaced relation by function - simplifies development
Sat, 28 Apr 2012 07:38:22 +0200 renamed Semi to Seq
Sun, 20 Nov 2011 21:05:23 +0100 eliminated obsolete "standard";
Thu, 03 Nov 2011 16:22:29 +1100 JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
Thu, 20 Oct 2011 12:30:43 -0400 removed [trans] concept from basic material
Wed, 19 Oct 2011 16:32:12 +0200 renamed B to Bc
Tue, 20 Sep 2011 05:48:23 +0200 Updated IMP to use new induction method
Mon, 12 Sep 2011 07:55:43 +0200 new fastforce replacing fastsimp - less confusing name
Mon, 08 Aug 2011 16:47:55 +0200 import constant folding theory into IMP
Mon, 01 Aug 2011 20:21:11 +0200 more consistent naming in IMP/Comp_Rev
Thu, 28 Jul 2011 16:56:14 +0200 compiler proof cleanup
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