# HG changeset patch
# User kleing
# Date 1017258303 -3600
# Node ID 0e028b1f3f38d77ecafa624d21643af1dce64a2f
# Parent  f538a1dba7ee41ad5eea4edc0be0f2a5bd9dd378
added lbv completeness

diff -r f538a1dba7ee -r 0e028b1f3f38 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Wed Mar 27 20:44:53 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Wed Mar 27 20:45:03 2002 +0100
@@ -14,7 +14,4 @@
 use_thy "BVSpecTypeSafe";
 use_thy "BVExample";
 use_thy "LBVCorrect";
-
-(* momentarily broken:
 use_thy "LBVComplete";
-*)