diff -r aeabb735883a -r 9864182c6bad doc-src/TutorialI/Protocol/Message.thy --- 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 \ (B \ A) = B \ A"