equal
deleted
inserted
replaced
3 Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson |
3 Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson |
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 = NatPair: |
8 theory MessageSET imports NatPair begin |
9 |
9 |
10 subsection{*General Lemmas*} |
10 subsection{*General Lemmas*} |
11 |
11 |
12 text{*Needed occasionally with @{text spy_analz_tac}, e.g. in |
12 text{*Needed occasionally with @{text spy_analz_tac}, e.g. in |
13 @{text analz_insert_Key_newK}*} |
13 @{text analz_insert_Key_newK}*} |