author | paulson |
Thu, 10 Jun 1999 10:36:41 +0200 | |
changeset 6807 | 6737af18317e |
parent 6806 | 43c081a0858d |
child 6808 | d5dfe040c183 |
--- 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)"