Trivial change to be more like paper
authorpaulson
Wed, 24 Jun 1998 10:30:29 +0200
changeset 5074 753d4daff1df
parent 5073 61e4403023a2
child 5075 9a3d48fa28ca
Trivial change to be more like paper
src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Wed Jun 24 10:29:46 1998 +0200
+++ b/src/HOL/Auth/TLS.thy	Wed Jun 24 10:30:29 1998 +0200
@@ -61,8 +61,8 @@
     clientK, serverK :: "nat*nat*nat => key"
 
 translations
-  "clientK (nonces)"	== "sessionK(nonces,0)"
-  "serverK (nonces)"	== "sessionK(nonces,1)"
+  "clientK X" == "sessionK(X,0)"
+  "serverK X" == "sessionK(X,1)"
 
 rules
   (*the pseudo-random function is collision-free*)