# HG changeset patch # User kleing # Date 1034078930 -7200 # Node ID c7cbb2b369b863265ec6f701e0ffe9a82120f9e8 # Parent 23ab136db946710c84b7928f0dc6cbc13a54186a defensive machine diff -r 23ab136db946 -r c7cbb2b369b8 src/HOL/MicroJava/ROOT.ML --- a/src/HOL/MicroJava/ROOT.ML Tue Oct 08 10:49:19 2002 +0200 +++ b/src/HOL/MicroJava/ROOT.ML Tue Oct 08 14:08:50 2002 +0200 @@ -10,7 +10,7 @@ use_thy "Example"; use_thy "JListExample"; use_thy "JVMListExample"; -use_thy "JVM"; +use_thy "JVMDefensive"; use_thy "LBVJVM"; -use_thy "BVSpecTypeSafe"; +use_thy "BVNoTypeError"; use_thy "BVExample";