author | paulson |
Wed, 24 Jun 1998 10:30:29 +0200 | |
changeset 5074 | 753d4daff1df |
parent 5073 | 61e4403023a2 |
child 5075 | 9a3d48fa28ca |
--- a/src/HOL/Auth/TLS.thy Wed Jun 24 10:29:46 1998 +0200 +++ b/src/HOL/Auth/TLS.thy Wed Jun 24 10:30:29 1998 +0200 @@ -61,8 +61,8 @@ clientK, serverK :: "nat*nat*nat => key" translations - "clientK (nonces)" == "sessionK(nonces,0)" - "serverK (nonces)" == "sessionK(nonces,1)" + "clientK X" == "sessionK(X,0)" + "serverK X" == "sessionK(X,1)" rules (*the pseudo-random function is collision-free*)