--- a/src/HOL/MicroJava/ROOT.ML Tue Aug 08 14:15:24 2000 +0200
+++ b/src/HOL/MicroJava/ROOT.ML Tue Aug 08 16:39:34 2000 +0200
@@ -5,4 +5,5 @@
Unify.trace_bound := 40;
with_paths ["J" ] use_thy "JTypeSafe";
+with_paths ["J" ] use_thy "Example";
with_paths ["J", "JVM", "BV"] use_thy "BVSpecTypeSafe";