diff -r 6a973bd43949 -r 1bc3b688548c src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Wed Dec 02 12:04:07 2009 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Tue Nov 24 14:37:23 2009 +0100
@@ -1,13 +1,13 @@
 (*  Title:      HOL/MicroJava/BV/EffMono.thy
-    ID:         $Id$
     Author:     Gerwin Klein
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
 header {* \isaheader{Monotonicity of eff and app} *}
 
-theory EffectMono imports Effect begin
-
+theory EffectMono
+imports Effect
+begin
 
 lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
   by (auto elim: widen.cases)