src/HOL/Auth/NS_Shared.thy
changeset 13956 8fe7e12290e1
parent 13935 4822d9597d1e
child 14200 d8598e24f8fa
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Mon May 05 15:55:56 2003 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Mon May 05 18:22:01 2003 +0200
     1.3 @@ -240,7 +240,7 @@
     1.4  
     1.5  subsubsection{*Crucial secrecy property: Spy does not see the keys sent in msg NS2*}
     1.6  
     1.7 -text{*Beware of [rule_format] and the universal quantifier!*}
     1.8 +text{*Beware of @{text "[rule_format]"} and the universal quantifier!*}
     1.9  lemma secrecy_lemma:
    1.10       "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
    1.11                                        Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)