diff -r d59bbf053258 -r 256f38c01b98 src/HOL/Auth/WooLam.thy
--- a/src/HOL/Auth/WooLam.thy Tue Jul 01 17:37:42 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy Tue Jul 01 17:38:49 1997 +0200
@@ -42,7 +42,7 @@
(*Alice responds to Bob's challenge by encrypting NB with her key.
B is *not* properly determined -- Alice essentially broadcasts
her reply.*)
- WL3 "[| evs: woolam; A ~= B;
+ WL3 "[| evs: woolam;
Says A B (Agent A) : set evs;
Says B' A (Nonce NB) : set evs |]
==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"