| changeset 28098 | c92850d2d16c |
| parent 27239 | f2f42f9fa09d |
| child 29888 | ab97183f1694 |
| 28097:003dff7410c1 | 28098:c92850d2d16c |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header{*The Message Theory, Modified for SET*} |
6 header{*The Message Theory, Modified for SET*} |
7 |
7 |
8 theory MessageSET |
8 theory MessageSET |
9 imports Main NatPair |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 subsection{*General Lemmas*} |
12 subsection{*General Lemmas*} |
13 |
13 |
14 text{*Needed occasionally with @{text spy_analz_tac}, e.g. in |
14 text{*Needed occasionally with @{text spy_analz_tac}, e.g. in |