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