src/HOL/MicroJava/BV/BVNoTypeError.thy
Thu, 12 Mar 2015 14:58:32 +0100 wenzelm quote "method" to allow Eisbach using this keyword;
Sun, 02 Nov 2014 17:58:35 +0100 wenzelm modernized header;
Tue, 09 Sep 2014 20:51:36 +0200 blanchet ported MicroJava to new datatypes
Thu, 13 Mar 2014 07:07:07 +0100 nipkow enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
Sun, 16 Feb 2014 21:33:28 +0100 blanchet folded 'list_all2' with the relator generated by 'datatype_new'
Tue, 13 Aug 2013 22:37:58 +0200 wenzelm more symbolic notation;
Tue, 13 Aug 2013 11:13:26 +0200 wenzelm tuned proofs;
Sun, 15 Jan 2012 18:55:27 +0100 wenzelm tuned proofs;
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Tue, 29 Mar 2011 17:30:26 +0200 wenzelm tuned headers;
Tue, 24 Nov 2009 14:37:23 +0100 haftmann backported parts of abstract byte code verifier from AFP/Jinja
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Fri, 28 Aug 2009 20:18:33 +0200 nipkow tuned proofs
Mon, 20 Aug 2007 17:46:31 +0200 wenzelm theory header: more precise imports;
Thu, 21 Jun 2007 22:10:16 +0200 wenzelm tuned proofs -- avoid implicit prems;
Wed, 07 Feb 2007 17:44:07 +0100 berghofe Adapted to new inductive definition package.
Tue, 03 Jan 2006 11:32:55 +0100 haftmann class now an keyword, quoted where necessary
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Thu, 19 Feb 2004 10:41:32 +0100 paulson moved list_all2I to List.thy
Mon, 26 May 2003 18:36:15 +0200 streckem Introduced distinction wf_prog vs. ws_prog
Tue, 18 Feb 2003 19:13:47 +0100 kleing check maxs in defensive machine
Thu, 24 Oct 2002 12:08:33 +0200 kleing changes for cleanup in JVM
Tue, 08 Oct 2002 14:09:18 +0200 kleing type safety with defensive machine
less more (0) tip