changeset 43564 | 9864182c6bad |
parent 42793 | 88bee9f6eec7 |
child 48895 | 4cd4ef1ef4a4 |
--- a/doc-src/TutorialI/Protocol/Message.thy Mon Jun 27 17:51:28 2011 +0200 +++ b/doc-src/TutorialI/Protocol/Message.thy Mon Jun 27 22:20:49 2011 +0200 @@ -9,6 +9,7 @@ header{*Theory of Agents and Messages for Security Protocols*} theory Message imports Main uses "../../antiquote_setup.ML" begin +setup {* Antiquote_Setup.setup *} (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"