equal
deleted
inserted
replaced
13 Cambridge CB3 0FD, United Kingdom |
13 Cambridge CB3 0FD, United Kingdom |
14 ******************************************************************************) |
14 ******************************************************************************) |
15 |
15 |
16 header{*Protocol P2*} |
16 header{*Protocol P2*} |
17 |
17 |
18 theory P2 = Guard_Public + List_Msg: |
18 theory P2 imports Guard_Public List_Msg begin |
19 |
19 |
20 subsection{*Protocol Definition*} |
20 subsection{*Protocol Definition*} |
21 |
21 |
22 |
22 |
23 text{*Like P1 except the definitions of @{text chain}, @{text shop}, |
23 text{*Like P1 except the definitions of @{text chain}, @{text shop}, |