# HG changeset patch
# User kleing
# Date 1008458394 -3600
# Node ID 6d754b9a1303d327213ecbe3809dd13681a6856d
# Parent  a955fe2879ba53579f62190f27a0a7d06a270e4e
temporarily removed JVMListExample

diff -r a955fe2879ba -r 6d754b9a1303 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";
+*)