# HG changeset patch
# User paulson
# Date 879243378 -3600
# Node ID c63639beeff19ed94dff6aac1fcc40b740cdce51
# Parent  1547bc6daa5aeaade2eb0d8d576dcb615ef9d48b
Fixed spelling error

diff -r 1547bc6daa5a -r c63639beeff1 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Tue Nov 11 11:15:51 1997 +0100
+++ b/src/HOL/Auth/TLS.thy	Tue Nov 11 11:16:18 1997 +0100
@@ -99,7 +99,7 @@
 	   NA is CLIENT RANDOM, while SID is SESSION_ID.
            UNIX TIME is omitted because the protocol doesn't use it.
            May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
-	   while MASTER SECRET is 48 byptes*)
+	   while MASTER SECRET is 48 bytes*)
          "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
           ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
 	        # evsCH  :  tls"