author | paulson |
Thu, 23 Jan 1997 10:35:28 +0100 | |
changeset 2538 | c55f68761a8d |
parent 2537 | 906704a5b3bf |
child 2539 | ddd22ceee8cc |
--- 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 +