diff -r 32c1deea5bcd -r b830bf10bf71 src/HOL/MicroJava/BV/BVSpec.thy
--- 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