| changeset 19363 | 667b5ea637dd |
| parent 16417 | 9bc16273c2d4 |
| child 21404 | eb85850d3eb7 |
--- a/src/HOL/Auth/Guard/Guard_Shared.thy Sat Apr 08 22:12:02 2006 +0200 +++ b/src/HOL/Auth/Guard/Guard_Shared.thy Sat Apr 08 22:51:06 2006 +0200 @@ -19,9 +19,9 @@ subsubsection{*a little abbreviation*} -syntax Ciph :: "agent => msg" - -translations "Ciph A X" == "Crypt (shrK A) X" +abbreviation + Ciph :: "agent => msg => msg" + "Ciph A X == Crypt (shrK A) X" subsubsection{*agent associated to a key*}