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.
rename_client_map_tac: avoid ill-defined thm reference;
authorwenzelm
Sun, 27 Jan 2008 22:21:39 +0100
changeset 25995 21b51f748daf
parent 25994 d35484265f46
child 25996 9fce1718825f
rename_client_map_tac: avoid ill-defined thm reference;
src/HOL/UNITY/Comp/Alloc.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/UNITY/Comp/Alloc.thy	Sun Jan 27 22:21:37 2008 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun Jan 27 22:21:39 2008 +0100
@@ -697,7 +697,7 @@
 {*
 fun rename_client_map_tac ss =
   EVERY [
-    simp_tac (ss addsimps [thm "rename_guarantees_eq_rename_inv"]) 1,
+    simp_tac (ss addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1,
     rtac @{thm guarantees_PLam_I} 1,
     assume_tac 2,
          (*preserves: routine reasoning*)
isabelle