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>"