src/HOL/MicroJava/BV/BVExample.thy
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Fri, 05 Aug 2011 14:16:44 +0200 Andreas Lochbihler replace old SML code generator by new code generator in MicroJava/JVM and /BV
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Sun, 24 Oct 2010 20:19:00 +0200 nipkow nat_number -> eval_nat_numeral
Thu, 20 May 2010 16:40:29 +0200 haftmann renamed List_Set to the now more appropriate More_Set
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Thu, 11 Feb 2010 00:45:02 +0100 wenzelm modernized translations;
Tue, 24 Nov 2009 14:37:23 +0100 haftmann backported parts of abstract byte code verifier from AFP/Jinja
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Mon, 29 Jun 2009 16:17:55 +0200 haftmann tuned
Mon, 29 Jun 2009 12:18:57 +0200 haftmann explicit Set constructor for code generated for sets
Mon, 18 May 2009 23:15:38 +0200 nipkow fine-tuned elimination of comprehensions involving x=t.
Sat, 16 May 2009 17:44:11 +0200 nipkow proof tuned
Sat, 16 May 2009 11:28:02 +0200 nipkow "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
Tue, 07 Oct 2008 16:07:25 +0200 haftmann tuned code setup
Mon, 20 Aug 2007 18:54:51 +0200 wenzelm theory header: fixed import;
Mon, 20 Aug 2007 17:46:31 +0200 wenzelm theory header: more precise imports;
Thu, 19 Jul 2007 21:47:39 +0200 haftmann uniform naming conventions for CG theories
Wed, 11 Jul 2007 11:32:02 +0200 berghofe - Renamed inductive2 to inductive
Sat, 19 May 2007 11:33:26 +0200 haftmann added qualification for ambiguous definition names
Wed, 07 Feb 2007 17:44:07 +0100 berghofe Adapted to new inductive definition package.
Tue, 31 Oct 2006 09:28:56 +0100 haftmann adapted to new serializer syntax
Tue, 10 Oct 2006 09:17:21 +0200 haftmann removed quote in serialization
Tue, 19 Sep 2006 15:21:52 +0200 haftmann added some stuff for code generation 2
Sun, 25 Sep 2005 20:15:29 +0200 berghofe Now uses set implementation from ExecutableSet.
Sat, 17 Sep 2005 18:11:25 +0200 wenzelm removed obsolete BasisLibrary;
Thu, 25 Aug 2005 16:13:09 +0200 berghofe Adapted to new code generator syntax.
Fri, 01 Jul 2005 14:10:02 +0200 berghofe Added BasisLibrary prefix to List.concat to avoid problems with
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
less more (0) -30 tip