src/HOL/Auth/TLS.thy
changeset 21404 eb85850d3eb7
parent 20768 1d478c2d621f
child 23746 a455e69c31cc
     1.1 --- a/src/HOL/Auth/TLS.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Auth/TLS.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -64,10 +64,11 @@
     1.4    sessionK :: "(nat*nat*nat) * role => key"
     1.5  
     1.6  abbreviation
     1.7 -  clientK :: "nat*nat*nat => key"
     1.8 +  clientK :: "nat*nat*nat => key" where
     1.9    "clientK X == sessionK(X, ClientRole)"
    1.10  
    1.11 -  serverK :: "nat*nat*nat => key"
    1.12 +abbreviation
    1.13 +  serverK :: "nat*nat*nat => key" where
    1.14    "serverK X == sessionK(X, ServerRole)"
    1.15  
    1.16