| changeset 13956 | 8fe7e12290e1 |
| parent 13922 | 75ae4244a596 |
| child 14200 | d8598e24f8fa |
--- a/src/HOL/Auth/NS_Public_Bad.thy Mon May 05 15:55:56 2003 +0200 +++ b/src/HOL/Auth/NS_Public_Bad.thy Mon May 05 18:22:01 2003 +0200 @@ -11,6 +11,8 @@ Proc. Royal Soc. 426 (1989) *) +header{*Verifying the Needham-Schroeder Public-Key Protocol*} + theory NS_Public_Bad = Public: consts ns_public :: "event list set"