src/HOL/Auth/WooLam.thy
changeset 2451 ce85a2aafc7a
parent 2283 68829cf138fc
child 2516 4d68fbe6378b
--- a/src/HOL/Auth/WooLam.thy	Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/WooLam.thy	Thu Dec 19 11:58:39 1996 +0100
@@ -37,7 +37,7 @@
          (*Bob responds to Alice's message with a challenge.*)
     WL2  "[| evs: woolam;  A ~= B;
              Says A' B (Agent A) : set_of_list evs |]
-          ==> Says B A (Nonce (newN evs)) # evs : woolam"
+          ==> Says B A (Nonce (newN(length evs))) # evs : woolam"
 
          (*Alice responds to Bob's challenge by encrypting NB with her key.
            B is *not* properly determined -- Alice essentially broadcasts