# HG changeset patch
# User paulson
# Date 898677029 -7200
# Node ID 753d4daff1dfd7cab66531e282f55cd383e7425a
# Parent  61e4403023a2bb0f2b99e6060ff5ed84e355fdfd
Trivial change to be more like paper

diff -r 61e4403023a2 -r 753d4daff1df 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*)