src/HOL/MicroJava/ROOT.ML

--- a/src/HOL/MicroJava/ROOT.ML	Sun Dec 16 00:19:08 2001 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Sun Dec 16 00:19:54 2001 +0100
@@ -7,8 +7,11 @@
 use_thy "JTypeSafe";
 use_thy "Example";
 use_thy "JListExample";
-use_thy "JVMListExample";
+(* use_thy "JVMListExample"; *)
 use_thy "BVSpecTypeSafe";
+use_thy "JVM";
+use_thy "LBVSpec"; 
+(* momentarily broken:
 use_thy "LBVCorrect";
 use_thy "LBVComplete";
-use_thy "JVM";
+*)