--- 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