equal
deleted
inserted
replaced
5 Inductive relations "parts", "analz" and "synth" |
5 Inductive relations "parts", "analz" and "synth" |
6 *)(*<*) |
6 *)(*<*) |
7 |
7 |
8 section\<open>Theory of Agents and Messages for Security Protocols\<close> |
8 section\<open>Theory of Agents and Messages for Security Protocols\<close> |
9 |
9 |
10 theory Message imports Main begin |
10 theory Message imports "../Setup" begin |
11 ML_file \<open>../../antiquote_setup.ML\<close> |
|
12 |
11 |
13 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) |
12 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) |
14 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A" |
13 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A" |
15 by blast |
14 by blast |
16 (*>*) |
15 (*>*) |