src/HOL/Auth/Message.thy
changeset 28698 b1c4366e1212
parent 27239 f2f42f9fa09d
child 30510 4120fc59dd85
equal deleted inserted replaced
28697:140bfb63f893 28698:b1c4366e1212
   104 
   104 
   105 
   105 
   106 subsubsection{*Inverse of keys *}
   106 subsubsection{*Inverse of keys *}
   107 
   107 
   108 lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
   108 lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
   109 apply safe
   109 by (metis invKey)
   110 apply (drule_tac f = invKey in arg_cong, simp)
       
   111 done
       
   112 
   110 
   113 
   111 
   114 subsection{*keysFor operator*}
   112 subsection{*keysFor operator*}
   115 
   113 
   116 lemma keysFor_empty [simp]: "keysFor {} = {}"
   114 lemma keysFor_empty [simp]: "keysFor {} = {}"