src/HOL/MicroJava/ROOT.ML

--- a/src/HOL/MicroJava/ROOT.ML	Thu Dec 07 18:22:17 2000 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Thu Dec 07 19:26:30 2000 +0100
@@ -7,4 +7,10 @@
 add_path "J";
 add_path "JVM";
 add_path "BV";
-use_thy "Digest"; 
+
+use_thy "JTypeSafe";
+use_thy "Example";
+use_thy "BVSpecTypeSafe";
+use_thy "LBVCorrect";
+use_thy "LBVComplete";
+use_thy "JVM";