equal
deleted
inserted
replaced
7 Inductive relations "parts", "analz" and "synth" |
7 Inductive relations "parts", "analz" and "synth" |
8 *) |
8 *) |
9 |
9 |
10 header{*Theory of Agents and Messages for Security Protocols*} |
10 header{*Theory of Agents and Messages for Security Protocols*} |
11 |
11 |
12 theory Message = Main: |
12 theory Message imports Main begin |
13 |
13 |
14 (*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*) |
15 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A" |
15 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A" |
16 by blast |
16 by blast |
17 |
17 |