--- a/src/HOL/MicroJava/BV/BVExample.thy Mon Dec 26 22:17:10 2011 +0100 +++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Dec 26 22:17:10 2011 +0100 @@ -9,7 +9,6 @@ "../JVM/JVMListExample" BVSpecTypeSafe JVM - "~~/src/HOL/Library/More_Set" begin text {*