src/HOL/Auth/TLS.thy
changeset 20768 1d478c2d621f
parent 16417 9bc16273c2d4
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Auth/TLS.thy	Thu Sep 28 23:42:32 2006 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Thu Sep 28 23:42:35 2006 +0200
     1.3 @@ -63,13 +63,13 @@
     1.4      Session keys implicitly include MAC secrets.*)
     1.5    sessionK :: "(nat*nat*nat) * role => key"
     1.6  
     1.7 -syntax
     1.8 -    clientK :: "nat*nat*nat => key"
     1.9 -    serverK :: "nat*nat*nat => key"
    1.10 +abbreviation
    1.11 +  clientK :: "nat*nat*nat => key"
    1.12 +  "clientK X == sessionK(X, ClientRole)"
    1.13  
    1.14 -translations
    1.15 -  "clientK X" == "sessionK(X, ClientRole)"
    1.16 -  "serverK X" == "sessionK(X, ServerRole)"
    1.17 +  serverK :: "nat*nat*nat => key"
    1.18 +  "serverK X == sessionK(X, ServerRole)"
    1.19 +
    1.20  
    1.21  specification (PRF)
    1.22    inj_PRF: "inj PRF"