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"