src/HOL/Auth/TLS.thy
changeset 5074 753d4daff1df
parent 4421 88639289be39
child 5359 bd539b72d484
     1.1 --- a/src/HOL/Auth/TLS.thy	Wed Jun 24 10:29:46 1998 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Wed Jun 24 10:30:29 1998 +0200
     1.3 @@ -61,8 +61,8 @@
     1.4      clientK, serverK :: "nat*nat*nat => key"
     1.5  
     1.6  translations
     1.7 -  "clientK (nonces)"	== "sessionK(nonces,0)"
     1.8 -  "serverK (nonces)"	== "sessionK(nonces,1)"
     1.9 +  "clientK X" == "sessionK(X,0)"
    1.10 +  "serverK X" == "sessionK(X,1)"
    1.11  
    1.12  rules
    1.13    (*the pseudo-random function is collision-free*)