# HG changeset patch
# User paulson
# Date 854373845 -3600
# Node ID 6e8d130463e3c4e698327bfce3b5904cbf07ca6f
# Parent  dffebc6ab0a1cf97fc71c0729b83422306009748
Corrected faulty comment

diff -r dffebc6ab0a1 -r 6e8d130463e3 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Mon Jan 27 15:01:17 1997 +0100
+++ b/src/HOL/Auth/NS_Shared.ML	Mon Jan 27 15:04:05 1997 +0100
@@ -241,8 +241,7 @@
 qed "analz_insert_freshK";
 
 
-(** The session key K uniquely identifies the message, if encrypted
-    with a secure key **)
+(** The session key K uniquely identifies the message **)
 
 goal thy 
  "!!evs. evs : ns_shared lost ==>                                        \