# HG changeset patch
# User kleing
# Date 1035758042 -3600
# Node ID 06cce9be31a43b78b8287de8bc0cacd9210cd033
# Parent  a6ce43a59d4acf8bee15e7a4c2f202c80467b97c
simplified lemma correct_frames_newref

diff -r a6ce43a59d4a -r 06cce9be31a4 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Sat Oct 26 13:05:27 2002 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Sun Oct 27 23:34:02 2002 +0100
@@ -334,8 +334,7 @@
   "\<forall>rT C sig. 
   hp x = None \<longrightarrow> 
   correct_frames G hp phi rT sig frs \<longrightarrow>
-  G,hp \<turnstile> obj \<surd>
-  \<longrightarrow> correct_frames G (hp(x \<mapsto> obj)) phi rT sig frs"
+  correct_frames G (hp(x \<mapsto> obj)) phi rT sig frs"
 apply (induct frs)
  apply simp
 apply clarify