diff -r 3fb416265ba9 -r d09d0f160888 src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy	Sun Dec 16 00:17:44 2001 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/BCV/Err.thy
+(*  Title:      HOL/MicroJava/BV/Err.thy
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2000 TUM
@@ -137,7 +137,8 @@
 
 lemma semilat_errI:
   "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
-apply (unfold semilat_Def closed_def plussub_def lesub_def lift2_def Err.le_def err_def)
+apply (unfold semilat_Def closed_def plussub_def lesub_def 
+              lift2_def Err.le_def err_def)
 apply (simp split: err.split)
 done