# HG changeset patch
# User kleing
# Date 969531948 -7200
# Node ID 8f228c148456e5bd045ab04beb54fc53ee75e26e
# Parent  22bf56fa9b44c6faebe15ccd590e79c018eff586
Digest.thy as toplevel theory

diff -r 22bf56fa9b44 -r 8f228c148456 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Thu Sep 21 12:25:07 2000 +0200
+++ b/src/HOL/MicroJava/ROOT.ML	Thu Sep 21 12:25:48 2000 +0200
@@ -4,8 +4,4 @@
 Unify.search_bound := 40;
 Unify.trace_bound  := 40;
 
-with_paths ["J"             ] use_thy "JTypeSafe";
-with_paths ["J"             ] use_thy "Example";
-with_paths ["J", "JVM", "BV"] use_thy "BVSpecTypeSafe";
-with_paths ["J", "JVM", "BV"] use_thy "LBVCorrect";
-with_paths ["J", "JVM", "BV"] use_thy "LBVComplete";
+with_paths ["J", "JVM", "BV"] use_thy "Digest";