--- a/src/HOL/Library/Code_Test.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Library/Code_Test.thy Fri Aug 12 17:53:55 2016 +0200
@@ -53,9 +53,10 @@
and (Scala) "_.mkString(\"\")"
text \<open>
- Stripped-down implementations of Isabelle's XML tree with YXML encoding
- as defined in @{file "~~/src/Pure/PIDE/xml.ML"}, @{file "~~/src/Pure/PIDE/yxml.ML"}
- sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}.
+ Stripped-down implementations of Isabelle's XML tree with YXML encoding as
+ defined in \<^file>\<open>~~/src/Pure/PIDE/xml.ML\<close>, \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close>
+ sufficient to encode @{typ "Code_Evaluation.term"} as in
+ \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
\<close>
datatype (plugins del: code size "quickcheck") xml_tree = XML_Tree
@@ -113,8 +114,8 @@
where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty"
text \<open>
- Encoding @{typ Code_Evaluation.term} into XML trees
- as defined in @{file "~~/src/Pure/term_xml.ML"}
+ Encoding @{typ Code_Evaluation.term} into XML trees as defined in
+ \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
\<close>
definition xml_of_typ :: "Typerep.typerep \<Rightarrow> xml.body"