src/HOL/MicroJava/BV/EffectMono.thy

--- a/src/HOL/MicroJava/BV/EffectMono.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -291,7 +291,7 @@
   
   note [simp] = eff_def
 
-  hence "G \<turnstile> (Some s1) <=' (Some s2)" by simp
+  with G have "G \<turnstile> (Some s1) <=' (Some s2)" by simp
   from this app2
   have app1: "app i G m rT pc et (Some s1)" by (rule app_mono)
 
@@ -439,4 +439,3 @@
 lemmas [iff del] = not_Err_eq
 
 end
-