equal
deleted
inserted
replaced
7 *)(*<*) |
7 *)(*<*) |
8 |
8 |
9 header{*Theory of Agents and Messages for Security Protocols*} |
9 header{*Theory of Agents and Messages for Security Protocols*} |
10 |
10 |
11 theory Message imports Main uses "../../antiquote_setup.ML" begin |
11 theory Message imports Main uses "../../antiquote_setup.ML" begin |
|
12 setup {* Antiquote_Setup.setup *} |
12 |
13 |
13 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) |
14 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) |
14 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A" |
15 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A" |
15 by blast |
16 by blast |
16 (*>*) |
17 (*>*) |