src/HOL/Auth/TLS.thy
changeset 3710 ea830f6e3c2d
parent 3704 2f99d7a0dccc
child 3729 6be7cf5086ab
     1.1 --- a/src/HOL/Auth/TLS.thy	Thu Sep 25 12:14:41 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Thu Sep 25 12:19:41 1997 +0200
     1.3 @@ -73,10 +73,6 @@
     1.4  
     1.5    isSym_sessionK "isSymKey (sessionK x)"
     1.6  
     1.7 -  (*serverK is similar*)
     1.8 -  inj_serverK   "inj serverK"	
     1.9 -  isSym_serverK "isSymKey (serverK x)"
    1.10 -
    1.11  
    1.12  consts    tls :: event list set
    1.13  inductive tls