src/HOL/MicroJava/BV/LBVCorrect.thy
Thu, 21 Jun 2007 20:07:26 +0200 wenzelm tuned proofs -- avoid implicit prems;
Wed, 06 Jun 2007 19:12:59 +0200 nipkow changed filter syntax from : to <-
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Wed, 22 Dec 2004 11:36:33 +0100 nipkow [ .. (] -> [ ..< ]
Tue, 15 Oct 2002 15:37:57 +0200 kleing alternative syntax
Tue, 16 Jul 2002 18:26:09 +0200 wenzelm adapted to locale defs;
Sat, 15 Jun 2002 22:57:33 +0200 kleing LBV instantiated for JVM
Tue, 11 Jun 2002 22:53:19 +0200 kleing stronger strong soundness
Tue, 11 Jun 2002 12:35:33 +0200 kleing included strong soundness (sound + s0 <= phi!0)
Thu, 04 Apr 2002 19:43:25 +0200 kleing tuned
Thu, 04 Apr 2002 16:48:00 +0200 kleing flattened, uses locales
Wed, 27 Mar 2002 20:44:53 +0100 kleing finished lbv completeness
Wed, 20 Mar 2002 13:21:07 +0100 kleing small refactoring for lbv with semilattices
Sun, 03 Mar 2002 16:59:08 +0100 kleing symbolized
Thu, 21 Feb 2002 09:54:08 +0100 kleing new document
less more (0) -15 tip