src/HOL/Auth/Shared.thy
changeset 17744 3007c82f17ca
parent 16417 9bc16273c2d4
child 18749 31c2af8b0c60
--- a/src/HOL/Auth/Shared.thy	Tue Oct 04 09:19:17 2005 +0200
+++ b/src/HOL/Auth/Shared.thy	Tue Oct 04 09:58:17 2005 +0200
@@ -103,7 +103,8 @@
 lemma shrK_neq [simp]: "Key K \<notin> used evs ==> shrK B \<noteq> K"
 by blast
 
-declare shrK_neq [THEN not_sym, simp]
+lemmas shrK_sym_neq = shrK_neq [THEN not_sym]
+declare shrK_sym_neq [simp]
 
 
 subsection{*Fresh nonces*}