equal
deleted
inserted
replaced
6 Inductive relations "parts", "analz" and "synth" |
6 Inductive relations "parts", "analz" and "synth" |
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 begin |
12 setup {* Antiquote_Setup.setup *} |
12 ML_file "../../antiquote_setup.ML" |
|
13 setup Antiquote_Setup.setup |
13 |
14 |
14 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) |
15 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) |
15 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A" |
16 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A" |
16 by blast |
17 by blast |
17 (*>*) |
18 (*>*) |