src/HOL/Auth/Shared.thy

--- a/src/HOL/Auth/Shared.thy	Mon Jan 23 10:34:38 2006 +0100
+++ b/src/HOL/Auth/Shared.thy	Mon Jan 23 11:36:05 2006 +0100
@@ -37,7 +37,8 @@
 subsection{*Basic properties of shrK*}
 
 (*Injectiveness: Agents' long-term keys are distinct.*)
-declare inj_shrK [THEN inj_eq, iff]
+lemmas shrK_injective = inj_shrK [THEN inj_eq]
+declare shrK_injective [iff]
 
 lemma invKey_K [simp]: "invKey K = K"
 apply (insert isSym_keys)