| changeset 58889 | 5b7a9633cfa8 |
| parent 58860 | fee7cfa69c50 |
| child 59498 | 50b60f501b05 |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
2 Author: Giampaolo Bella |
2 Author: Giampaolo Bella |
3 Author: Fabio Massacci |
3 Author: Fabio Massacci |
4 Author: Lawrence C Paulson |
4 Author: Lawrence C Paulson |
5 *) |
5 *) |
6 |
6 |
7 header{*The Message Theory, Modified for SET*} |
7 section{*The Message Theory, Modified for SET*} |
8 |
8 |
9 theory Message_SET |
9 theory Message_SET |
10 imports Main "~~/src/HOL/Library/Nat_Bijection" |
10 imports Main "~~/src/HOL/Library/Nat_Bijection" |
11 begin |
11 begin |
12 |
12 |