src/HOL/Auth/Message.thy
changeset 6807 6737af18317e
parent 5652 fe5f5510aef4
child 7057 b9ddbb925939
equal deleted inserted replaced
6806:43c081a0858d 6807:6737af18317e
    52 
    52 
    53 translations
    53 translations
    54   "Agent x"   == "Atomic (AGENT x)"
    54   "Agent x"   == "Atomic (AGENT x)"
    55   "Number x"  == "Atomic (NUMBER x)"
    55   "Number x"  == "Atomic (NUMBER x)"
    56   "Nonce x"   == "Atomic (NONCE x)"
    56   "Nonce x"   == "Atomic (NONCE x)"
       
    57   "Nonce``x"  == "Atomic `` (NONCE `` x)"
    57   "Key x"     == "Atomic (KEY x)"
    58   "Key x"     == "Atomic (KEY x)"
    58   "Key``x"    == "Atomic `` (KEY `` x)"
    59   "Key``x"    == "Atomic `` (KEY `` x)"
    59 
    60 
    60 
    61 
    61 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    62 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)