src/HOL/Auth/TLS.thy
changeset 11230 756c5034f08b
parent 11185 1b737b4c2108
child 11287 0103ee3082bf
     1.1 --- a/src/HOL/Auth/TLS.thy	Wed Mar 28 13:40:06 2001 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Thu Mar 29 10:44:37 2001 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4    inj_sessionK  "inj sessionK"	
     1.5  
     1.6    (*sessionK makes symmetric keys*)
     1.7 -  isSym_sessionK "isSymKey (sessionK nonces)"
     1.8 +  isSym_sessionK "sessionK nonces \\<in> symKeys"
     1.9  
    1.10  
    1.11  consts    tls :: event list set