Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/BV/Correct.thy
changeset 59199 cb8e5f7a5e4a
parent 58886 8a6cac7c7247
child 60773 d09c66a0ea10 
--- a/src/HOL/MicroJava/BV/Correct.thy	Mon Dec 29 20:51:42 2014 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Mon Dec 29 21:02:49 2014 +0100
@@ -175,7 +175,7 @@
 lemma approx_stk_rev_lem:
   "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
   apply (unfold approx_stk_def approx_loc_def)
-  apply (simp add: rev_map [THEN sym])
+  apply (simp add: rev_map [symmetric])
   done
 
 lemma approx_stk_rev:
isabelle