# HG changeset patch
# User oheimb
# Date 965745574 -7200
# Node ID c1e730bebcaab75cfb63101471fe6efc130a97e3
# Parent  dcdcfb0545e0b6e631f44c4e51c558fcbdcdf04a
added Example

diff -r dcdcfb0545e0 -r c1e730bebcaa src/HOL/MicroJava/ROOT.ML
--- 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";