src/HOL/Auth/Message.thy
changeset 6807 6737af18317e
parent 5652 fe5f5510aef4
child 7057 b9ddbb925939
--- 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)"