| changeset 28098 | c92850d2d16c |
| parent 23746 | a455e69c31cc |
| child 29888 | ab97183f1694 |
--- a/src/HOL/Auth/TLS.thy Tue Sep 02 22:20:27 2008 +0200 +++ b/src/HOL/Auth/TLS.thy Tue Sep 02 22:37:20 2008 +0200 @@ -41,7 +41,7 @@ header{*The TLS Protocol: Transport Layer Security*} -theory TLS imports Public NatPair begin +theory TLS imports Public begin constdefs certificate :: "[agent,key] => msg"