src/HOL/Auth/Message.thy
changeset 1947 f19a801a2bca
parent 1913 2809adb15eb0
child 2010 0a22b9d63a18
equal deleted inserted replaced
1946:b59a3d686436 1947:f19a801a2bca
    53       | MPair msg msg
    53       | MPair msg msg
    54       | Crypt msg key
    54       | Crypt msg key
    55 
    55 
    56 (*Allows messages of the form {|A,B,NA|}, etc...*)
    56 (*Allows messages of the form {|A,B,NA|}, etc...*)
    57 syntax
    57 syntax
    58   "@MTuple"      :: "['a, args] => 'a * 'b"            ("(1{|_,/ _|})")
    58   "@MTuple"      :: "['a, args] => 'a * 'b"            ("(2{|_,/ _|})")
    59 
    59 
    60 translations
    60 translations
    61   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    61   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    62   "{|x, y|}"      == "MPair x y"
    62   "{|x, y|}"      == "MPair x y"
    63 
    63