src/HOL/Auth/TLS.thy

--- a/src/HOL/Auth/TLS.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/TLS.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -41,7 +41,7 @@
 
 header{*The TLS Protocol: Transport Layer Security*}
 
-theory TLS = Public + NatPair:
+theory TLS imports Public NatPair begin
 
 constdefs
   certificate      :: "[agent,key] => msg"