--- a/src/HOL/MicroJava/BV/BVSpec.thy Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Fri Feb 09 16:01:58 2001 +0100
@@ -58,9 +58,6 @@
(app i G mxs rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
by (simp add: wt_instr_def)
-
-
-
end