# HG changeset patch
# User kleing
# Date 976213590 -3600
# Node ID 591ea23d27a03fe68758adb726fc635ddc03ad78
# Parent  f89c3fc4fde19b75d122685f081c4352d5265947
removed Digest (temporarily, not up to date)
added theory JVM

diff -r f89c3fc4fde1 -r 591ea23d27a0 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";