src/HOL/Auth/Guard/Guard_Shared.thy
changeset 19363 667b5ea637dd
parent 16417 9bc16273c2d4
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Auth/Guard/Guard_Shared.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -19,9 +19,9 @@
     1.4  
     1.5  subsubsection{*a little abbreviation*}
     1.6  
     1.7 -syntax Ciph :: "agent => msg"
     1.8 -
     1.9 -translations "Ciph A X" == "Crypt (shrK A) X"
    1.10 +abbreviation
    1.11 +  Ciph :: "agent => msg => msg"
    1.12 +  "Ciph A X == Crypt (shrK A) X"
    1.13  
    1.14  subsubsection{*agent associated to a key*}
    1.15