changeset 69605 | a96320074298 |
parent 69597 | ff784d5a5bfb |
child 72991 | d0a0b74f0ad7 |
--- a/src/Doc/Tutorial/Protocol/Message.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/Doc/Tutorial/Protocol/Message.thy Sun Jan 06 15:04:34 2019 +0100 @@ -8,7 +8,7 @@ section\<open>Theory of Agents and Messages for Security Protocols\<close> theory Message imports Main begin -ML_file "../../antiquote_setup.ML" +ML_file \<open>../../antiquote_setup.ML\<close> (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"