metis proof
authorpaulson
Mon Oct 27 18:14:34 2008 +0100 (2008-10-27)
changeset 28698b1c4366e1212
parent 28697 140bfb63f893
child 28699 32b6a8f12c1c
metis proof
src/HOL/Auth/Message.thy
     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*}