Deleted obsolete axioms inj_serverK and isSym_serverK
authorpaulson
Thu Sep 25 12:19:41 1997 +0200 (1997-09-25)
changeset 3710ea830f6e3c2d
parent 3709 c13c2137e9ee
child 3711 2f86b403d975
Deleted obsolete axioms inj_serverK and isSym_serverK
src/HOL/Auth/TLS.thy
     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