removed Digest (temporarily, not up to date)
authorkleing
Thu, 07 Dec 2000 19:26:30 +0100
changeset 10631 591ea23d27a0
parent 10630 f89c3fc4fde1
child 10632 e887eca23edb
removed Digest (temporarily, not up to date) added theory JVM
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";