| changeset 29888 | ab97183f1694 |
| parent 28098 | c92850d2d16c |
| child 30510 | 4120fc59dd85 |
| 29886:b8a6b9c56fdd | 29888:ab97183f1694 |
|---|---|
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 |
9 imports Main Nat_Int_Bij |
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 |