author | paulson |
Mon, 27 Jan 1997 15:04:05 +0100 | |
changeset 2558 | 6e8d130463e3 |
parent 2557 | dffebc6ab0a1 |
child 2559 | 06b6a499f8ae |
--- 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 ==> \