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 imports NatPair begin |
8 theory MessageSET |
|
9 imports Main NatPair |
|
10 begin |
9 |
11 |
10 subsection{*General Lemmas*} |
12 subsection{*General Lemmas*} |
11 |
13 |
12 text{*Needed occasionally with @{text spy_analz_tac}, e.g. in |
14 text{*Needed occasionally with @{text spy_analz_tac}, e.g. in |
13 @{text analz_insert_Key_newK}*} |
15 @{text analz_insert_Key_newK}*} |