equal
deleted
inserted
replaced
6 Theory of Public Keys (common to all public-key protocols) |
6 Theory of Public Keys (common to all public-key protocols) |
7 |
7 |
8 Private and public keys; initial states of agents |
8 Private and public keys; initial states of agents |
9 *) |
9 *) |
10 |
10 |
11 theory Public = Event |
11 theory Public imports Event |
12 files ("Public_lemmas.ML"): |
12 uses ("Public_lemmas.ML") begin |
13 |
13 |
14 consts |
14 consts |
15 pubK :: "agent => key" |
15 pubK :: "agent => key" |
16 |
16 |
17 syntax |
17 syntax |