diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/TLS.thy	Thu Mar 29 10:44:37 2001 +0200
@@ -72,7 +72,7 @@
   inj_sessionK  "inj sessionK"	
 
   (*sessionK makes symmetric keys*)
-  isSym_sessionK "isSymKey (sessionK nonces)"
+  isSym_sessionK "sessionK nonces \\<in> symKeys"
 
 
 consts    tls :: event list set