| changeset 16417 | 9bc16273c2d4 |
| parent 14200 | d8598e24f8fa |
| child 23746 | a455e69c31cc |
--- a/src/HOL/Auth/NS_Public_Bad.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Auth/NS_Public_Bad.thy Fri Jun 17 16:12:49 2005 +0200 @@ -13,7 +13,7 @@ header{*Verifying the Needham-Schroeder Public-Key Protocol*} -theory NS_Public_Bad = Public: +theory NS_Public_Bad imports Public begin consts ns_public :: "event list set"