src/HOL/Auth/NS_Public.thy

--- a/src/HOL/Auth/NS_Public.thy	Thu Jan 23 10:35:03 1997 +0100
+++ b/src/HOL/Auth/NS_Public.thy	Thu Jan 23 10:35:28 1997 +0100
@@ -4,7 +4,7 @@
     Copyright   1996  University of Cambridge
 
 Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
-Version incorporating Lowe's fix (inclusion of B's identify in round 2).
+Version incorporating Lowe's fix (inclusion of B's identity in round 2).
 *)
 
 NS_Public = Public +