src/HOL/Auth/Message.thy
changeset 28698 b1c4366e1212
parent 27239 f2f42f9fa09d
child 30510 4120fc59dd85
     1.1 --- a/src/HOL/Auth/Message.thy	Mon Oct 27 16:23:54 2008 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Mon Oct 27 18:14:34 2008 +0100
     1.3 @@ -106,9 +106,7 @@
     1.4  subsubsection{*Inverse of keys *}
     1.5  
     1.6  lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
     1.7 -apply safe
     1.8 -apply (drule_tac f = invKey in arg_cong, simp)
     1.9 -done
    1.10 +by (metis invKey)
    1.11  
    1.12  
    1.13  subsection{*keysFor operator*}