changeset 2122 | cb302f6c9c06 |
parent 2103 | bfd2e8cca89c |
child 2131 | 3106a99d30a5 |
--- a/src/HOL/Auth/NS_Shared.ML Thu Oct 24 10:30:43 1996 +0200 +++ b/src/HOL/Auth/NS_Shared.ML Thu Oct 24 10:31:17 1996 +0200 @@ -387,8 +387,6 @@ (** The session key K uniquely identifies the message, if encrypted with a secure key **) -fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1); - goal thy "!!evs. evs : ns_shared lost ==> \ \ EX A' NA' B' X'. ALL A NA B X. \