src/HOL/Auth/TLS.thy
changeset 41413 64cd30d6b0b8
parent 37936 1e4c5015a72e
child 41774 13b97824aec6
     1.1 --- a/src/HOL/Auth/TLS.thy	Wed Dec 29 13:51:17 2010 +0100
     1.2 +++ b/src/HOL/Auth/TLS.thy	Wed Dec 29 17:34:41 2010 +0100
     1.3 @@ -40,7 +40,7 @@
     1.4  
     1.5  header{*The TLS Protocol: Transport Layer Security*}
     1.6  
     1.7 -theory TLS imports Public Nat_Bijection begin
     1.8 +theory TLS imports Public "~~/src/HOL/Library/Nat_Bijection" begin
     1.9  
    1.10  definition certificate :: "[agent,key] => msg" where
    1.11      "certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}"