# HG changeset patch
# User paulson
# Date 1128412697 -7200
# Node ID 3007c82f17cadd9ed7091bfc22151a0104d8bf4d
# Parent  f546af04142a45c22f6fdbeea7b292d2d4d1df5c
theorems need names

diff -r f546af04142a -r 3007c82f17ca src/HOL/Auth/Shared.thy
--- 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*}