Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proof;
authorwenzelm
Fri, 23 Sep 2011 13:43:44 +0200
changeset 45054 73accf69135d
parent 45053 54c832311598
child 45055 55274f7e306b
tuned proof;
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Fri Sep 23 10:31:12 2011 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Fri Sep 23 13:43:44 2011 +0200
@@ -1270,7 +1270,7 @@
 lemma correct_state_impl_Some_method:
   "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
   \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
-by (auto simp add: correct_state_def Let_def)
+by (auto simp add: correct_state_def)
 
 
 lemma BV_correct_1 [rule_format]:
isabelle