equal
deleted
inserted
replaced
18 declare initState.simps [simp del] |
18 declare initState.simps [simp del] |
19 |
19 |
20 subsubsection{*a little abbreviation*} |
20 subsubsection{*a little abbreviation*} |
21 |
21 |
22 abbreviation |
22 abbreviation |
23 Ciph :: "agent => msg => msg" |
23 Ciph :: "agent => msg => msg" where |
24 "Ciph A X == Crypt (shrK A) X" |
24 "Ciph A X == Crypt (shrK A) X" |
25 |
25 |
26 subsubsection{*agent associated to a key*} |
26 subsubsection{*agent associated to a key*} |
27 |
27 |
28 constdefs agt :: "key => agent" |
28 constdefs agt :: "key => agent" |