src/HOL/IMP/Compiler.thy
Tue, 20 Nov 2012 17:49:26 +0100 nipkow tuned proof
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
Fri, 25 Nov 2011 12:18:33 +0100 nipkow tuned
Wed, 23 Nov 2011 07:44:56 +0100 nipkow tuned
Thu, 03 Nov 2011 18:10:13 +1100 kleing string -> vname
Thu, 03 Nov 2011 16:22:29 +1100 kleing JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
Wed, 19 Oct 2011 16:32:12 +0200 nipkow renamed B to Bc
Wed, 12 Oct 2011 20:16:48 +0200 wenzelm tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
Thu, 29 Sep 2011 21:42:03 +0200 Jean Pichon fixed typos in IMP
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
Thu, 04 Aug 2011 16:49:57 +0200 kleing new state syntax with less conflicts
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
Mon, 06 Jun 2011 16:29:38 +0200 kleing imported rest of new IMP
Wed, 01 Jun 2011 21:35:34 +0200 nipkow Replacing old IMP with new Semantics material
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Thu, 09 Jul 2009 17:33:22 +0200 krauss drop unused lemmas
Wed, 25 Jun 2008 22:01:34 +0200 wenzelm modernized specifications;
Wed, 11 Jul 2007 11:14:51 +0200 berghofe Adapted to new inductive definition package.
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Tue, 11 May 2004 20:11:08 +0200 obua changes made due to new Ring_and_Field theory
Thu, 24 Oct 2002 07:23:46 +0200 nipkow ASIN -> SET
Tue, 08 Oct 2002 08:20:17 +0200 nipkow Got rid of rotates because of new simplifier
Fri, 26 Apr 2002 11:47:01 +0200 nipkow New machine architecture and other direction of compiler proof.
Thu, 20 Dec 2001 18:22:44 +0100 nipkow renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
Wed, 19 Dec 2001 00:26:04 +0100 wenzelm tuned;
Sun, 09 Dec 2001 14:34:56 +0100 kleing tuned for latex output
Fri, 23 Nov 2001 17:19:14 +0100 nipkow Isar conversion
Sat, 06 Oct 2001 00:02:46 +0200 wenzelm * sane numerals (stage 2): plain "num" syntax (removed "#");
Fri, 05 Oct 2001 21:52:39 +0200 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
Mon, 30 Apr 2001 19:26:04 +0200 nipkow new proof
Fri, 10 Nov 2000 09:17:54 +0100 nipkow JMB -> JMPB. Email von Johannes Pfeifroth.
Thu, 26 Oct 2000 14:59:38 +0200 nipkow *** empty log message ***
Thu, 26 Oct 2000 14:52:41 +0200 nipkow *** empty log message ***
less more (0) tip