src/HOL/MicroJava/ROOT.ML

--- a/src/HOL/MicroJava/ROOT.ML	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Thu Feb 21 09:54:08 2002 +0100
@@ -4,15 +4,17 @@
 add_path "JVM";
 add_path "BV";
 
+no_document use_thy "While_Combinator";
+
 use_thy "JTypeSafe";
 use_thy "Example";
 use_thy "JListExample";
 use_thy "JVMListExample";
 use_thy "BVSpecTypeSafe";
 use_thy "JVM";
-use_thy "LBVSpec"; 
 
 (* momentarily broken:
+use_thy "LBVSpec"; 
 use_thy "LBVCorrect";
 use_thy "LBVComplete";
 *)