src/Doc/Tutorial/Protocol/Message.thy
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"