src/HOL/Auth/Message.thy
changeset 10833 c0844a30ea4e
parent 9686 87b460d72e80
child 11189 1ea763a5d186
     1.1 --- a/src/HOL/Auth/Message.thy	Tue Jan 09 15:22:13 2001 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Tue Jan 09 15:29:17 2001 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4  
     1.5    (*Keys useful to decrypt elements of a message set*)
     1.6    keysFor :: msg set => key set
     1.7 -  "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
     1.8 +  "keysFor H == invKey ` {K. EX X. Crypt K X : H}"
     1.9  
    1.10  (** Inductive definition of all "parts" of a message.  **)
    1.11