# HG changeset patch
# User paulson
# Date 1225127674 -3600
# Node ID b1c4366e1212b4ae46fb92b2fdba496a67690d8f
# Parent  140bfb63f8936b54134667cf2deabab05ff10df1
metis proof

diff -r 140bfb63f893 -r b1c4366e1212 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Mon Oct 27 16:23:54 2008 +0100
+++ b/src/HOL/Auth/Message.thy	Mon Oct 27 18:14:34 2008 +0100
@@ -106,9 +106,7 @@
 subsubsection{*Inverse of keys *}
 
 lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
-apply safe
-apply (drule_tac f = invKey in arg_cong, simp)
-done
+by (metis invKey)
 
 
 subsection{*keysFor operator*}