src/HOL/MicroJava/J/State.thy
Fri, 05 Aug 2011 14:16:44 +0200 Andreas Lochbihler replace old SML code generator by new code generator in MicroJava/JVM and /BV
Sat, 23 Apr 2011 13:00:19 +0200 wenzelm modernized specifications;
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, 11 Aug 2009 10:46:11 +0200 haftmann dropped temporary adjustments to non-working eta expansion in recfun_codegen.ML
Tue, 11 Aug 2009 10:05:16 +0200 haftmann temporary adjustment to dubious state of eta expansion in recfun_codegen
Wed, 04 Mar 2009 10:47:20 +0100 nipkow Made Option a separate theory and renamed option_map to Option.map
Sun, 30 Sep 2007 21:55:15 +0200 wenzelm avoid internal names;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Fri, 29 Aug 2003 15:19:02 +0200 ballarin Methods rule_tac etc support static (Isar) contexts.
Fri, 08 Aug 2003 15:05:11 +0200 streckem added lemma c_hupd_fst
Fri, 25 Jul 2003 17:21:22 +0200 nipkow Replaced \<leadsto> by \<rightharpoonup>
Wed, 23 Oct 2002 16:09:02 +0200 streckem Added compiler
Thu, 21 Feb 2002 09:54:08 +0100 kleing new document
Tue, 18 Dec 2001 21:28:01 +0100 kleing removed preallocated heaps axiom (now in type safety invariant)
Sun, 16 Dec 2001 00:18:17 +0100 kleing exception merge, cleanup, tuned
less more (0) -16 tip