# HG changeset patch
# User paulson
# Date 905934534 -7200
# Node ID e335c51808accdf96a67d89f70215490331761a3
# Parent  d9fc3457554e9ab3a490e0c89a7cf2a71373c208
deleted redundant quantifiers

diff -r d9fc3457554e -r e335c51808ac src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Tue Sep 15 15:10:38 1998 +0200
+++ b/src/HOL/Auth/Message.ML	Wed Sep 16 10:28:54 1998 +0200
@@ -33,7 +33,7 @@
 
 (** Inverse of keys **)
 
-Goal "!!K K'. (invKey K = invKey K') = (K=K')";
+Goal "(invKey K = invKey K') = (K=K')";
 by Safe_tac;
 by (rtac box_equals 1);
 by (REPEAT (rtac invKey 2));