src/HOL/Auth/TLS.thy
changeset 66453 cc19f7ca2ed6
parent 61977 f55f28132128
child 67443 3abf6a722518
--- a/src/HOL/Auth/TLS.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Auth/TLS.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -40,7 +40,7 @@
 
 section\<open>The TLS Protocol: Transport Layer Security\<close>
 
-theory TLS imports Public "~~/src/HOL/Library/Nat_Bijection" begin
+theory TLS imports Public "HOL-Library.Nat_Bijection" begin
 
 definition certificate :: "[agent,key] => msg" where
     "certificate A KA == Crypt (priSK Server) \<lbrace>Agent A, Key KA\<rbrace>"