src/Doc/Tutorial/Protocol/Message.thy
changeset 72991 d0a0b74f0ad7
parent 69605 a96320074298
child 80768 c7723cc15de8
--- a/src/Doc/Tutorial/Protocol/Message.thy	Wed Dec 23 22:25:22 2020 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Wed Dec 23 23:03:03 2020 +0100
@@ -7,8 +7,7 @@
 
 section\<open>Theory of Agents and Messages for Security Protocols\<close>
 
-theory Message imports Main begin
-ML_file \<open>../../antiquote_setup.ML\<close>
+theory Message imports "../Setup" begin
 
 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"