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