# HG changeset patch
# User kleing
# Date 1014916583 -3600
# Node ID 16cc829b9c6520b84ab0a1d50a6c16340a827953
# Parent  fcc9a30a7ef219e205e7ccc095b0480943ff7b90
included LBVSpec again

diff -r fcc9a30a7ef2 -r 16cc829b9c65 src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Feb 28 18:11:11 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Feb 28 18:16:23 2002 +0100
@@ -15,7 +15,9 @@
   soundness and completeness are broken (they still need to be
   ported to the exception version). Both theories are included
   for documentation (but they don't work for this specification), 
-  please see the Isabelle 99-2 release for a working copy.
+  please see the Isabelle 99-2 release for a working copy, or
+  \url{http://isabelle.in.tum.de/verificard} for the most recent
+  development of \mJava.
 *}
 
 types
diff -r fcc9a30a7ef2 -r 16cc829b9c65 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Thu Feb 28 18:11:11 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Thu Feb 28 18:16:23 2002 +0100
@@ -13,9 +13,9 @@
 use_thy "JVM";
 use_thy "BVSpecTypeSafe";
 use_thy "BVExample";
+use_thy "LBVSpec"; 
 
 (* momentarily broken:
-use_thy "LBVSpec"; 
 use_thy "LBVCorrect";
 use_thy "LBVComplete";
 *)