src/HOL/Auth/Message.thy
changeset 6807 6737af18317e
parent 5652 fe5f5510aef4
child 7057 b9ddbb925939
     1.1 --- a/src/HOL/Auth/Message.thy	Thu Jun 10 10:35:58 1999 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Thu Jun 10 10:36:41 1999 +0200
     1.3 @@ -54,6 +54,7 @@
     1.4    "Agent x"   == "Atomic (AGENT x)"
     1.5    "Number x"  == "Atomic (NUMBER x)"
     1.6    "Nonce x"   == "Atomic (NONCE x)"
     1.7 +  "Nonce``x"  == "Atomic `` (NONCE `` x)"
     1.8    "Key x"     == "Atomic (KEY x)"
     1.9    "Key``x"    == "Atomic `` (KEY `` x)"
    1.10