src/HOL/Auth/Shared.thy
changeset 17744 3007c82f17ca
parent 16417 9bc16273c2d4
child 18749 31c2af8b0c60
equal deleted inserted replaced
17743:f546af04142a 17744:3007c82f17ca
   101 by blast
   101 by blast
   102 
   102 
   103 lemma shrK_neq [simp]: "Key K \<notin> used evs ==> shrK B \<noteq> K"
   103 lemma shrK_neq [simp]: "Key K \<notin> used evs ==> shrK B \<noteq> K"
   104 by blast
   104 by blast
   105 
   105 
   106 declare shrK_neq [THEN not_sym, simp]
   106 lemmas shrK_sym_neq = shrK_neq [THEN not_sym]
       
   107 declare shrK_sym_neq [simp]
   107 
   108 
   108 
   109 
   109 subsection{*Fresh nonces*}
   110 subsection{*Fresh nonces*}
   110 
   111 
   111 lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
   112 lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"