src/HOL/MicroJava/BV/BVSpec.thy

--- a/src/HOL/MicroJava/BV/BVSpec.thy	Fri Jul 25 12:03:28 2008 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Fri Jul 25 12:03:31 2008 +0200
@@ -7,7 +7,9 @@
 
 header {* \isaheader{The Bytecode Verifier}\label{sec:BVSpec} *}
 
-theory BVSpec imports Effect begin
+theory BVSpec
+imports Effect
+begin
 
 text {*
   This theory contains a specification of the BV. The specification