# HG changeset patch
# User paulson
# Date 929003801 -7200
# Node ID 6737af18317e4c6f777d20cf9e23e5221bf3a392
# Parent  43c081a0858d57e4bb4534897d4c38aa7c75315d
new translation to allow images over Nonce

diff -r 43c081a0858d -r 6737af18317e src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Thu Jun 10 10:35:58 1999 +0200
+++ b/src/HOL/Auth/Message.thy	Thu Jun 10 10:36:41 1999 +0200
@@ -54,6 +54,7 @@
   "Agent x"   == "Atomic (AGENT x)"
   "Number x"  == "Atomic (NUMBER x)"
   "Nonce x"   == "Atomic (NONCE x)"
+  "Nonce``x"  == "Atomic `` (NONCE `` x)"
   "Key x"     == "Atomic (KEY x)"
   "Key``x"    == "Atomic `` (KEY `` x)"