src/HOL/Auth/Message.thy
changeset 2516 4d68fbe6378b
parent 2484 596a5b5a68ff
child 3668 a39baf59ea47
     1.1 --- a/src/HOL/Auth/Message.thy	Fri Jan 17 11:50:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Fri Jan 17 12:49:31 1997 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5  (*Allows messages of the form {|A,B,NA|}, etc...*)
     1.6  syntax
     1.7 -  "@MTuple"      :: "['a, args] => 'a * 'b"            ("(2{|_,/ _|})")
     1.8 +  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     1.9  
    1.10  translations
    1.11    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    1.12 @@ -50,8 +50,8 @@
    1.13  
    1.14  constdefs
    1.15    (*Message Y, paired with a MAC computed with the help of X*)
    1.16 -  HPair :: "[msg,msg]=>msg"
    1.17 -    "HPair X Y == {| Hash{|X,Y|}, Y|}"
    1.18 +  HPair :: "[msg,msg]=>msg"                       ("(4Hash[_] /_)" [0, 1000])
    1.19 +    "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
    1.20  
    1.21    (*Keys useful to decrypt elements of a message set*)
    1.22    keysFor :: msg set => key set