src/HOL/IMP/Compiler.thy
Thu, 10 Sep 2015 11:03:29 +0200 nipkow tuned
Mon, 22 Jun 2015 16:56:03 +0200 blanchet fixed typo
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Tue, 09 Sep 2014 20:51:36 +0200 blanchet use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
Wed, 19 Feb 2014 22:02:00 +1100 kleing tuned definition
Thu, 14 Nov 2013 10:59:22 +0100 nipkow tuned to improve automation (for REPEAT)
Fri, 27 Sep 2013 17:57:30 +0200 nipkow hide coercion
Wed, 25 Sep 2013 15:49:09 +0200 nipkow tuned
Wed, 25 Sep 2013 11:56:33 +0200 nipkow tuned
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Sat, 10 Aug 2013 10:15:30 +0200 kleing avoid unnecessary case distinction
Fri, 09 Aug 2013 12:27:29 +0200 kleing removed commented out declaration
Thu, 08 Aug 2013 18:13:12 +0200 kleing avoid re-inventing transitive closure
Thu, 08 Aug 2013 14:47:24 +0200 kleing snippet for instr type
Fri, 17 May 2013 08:19:52 +0200 nipkow replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
Sun, 24 Feb 2013 13:46:14 +1100 kleing eliminated isize in favour of size + type coercion
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