| changeset 35101 | 6ce9177d6b38 |
| parent 33028 | 9aa8bfb1649d |
| child 39758 | b8a53e3a0ee2 |
| 35100:53754ec7360b | 35101:6ce9177d6b38 |
|---|---|
9 theory Event_SET |
9 theory Event_SET |
10 imports Message_SET |
10 imports Message_SET |
11 begin |
11 begin |
12 |
12 |
13 text{*The Root Certification Authority*} |
13 text{*The Root Certification Authority*} |
14 syntax RCA :: agent |
14 abbreviation "RCA == CA 0" |
15 translations "RCA" == "CA 0" |
|
16 |
15 |
17 |
16 |
18 text{*Message events*} |
17 text{*Message events*} |
19 datatype |
18 datatype |
20 event = Says agent agent msg |
19 event = Says agent agent msg |