--- a/doc-src/System/Thy/document/Misc.tex Wed Sep 07 17:42:57 2011 +0200
+++ b/doc-src/System/Thy/document/Misc.tex Wed Sep 07 18:01:01 2011 +0200
@@ -376,8 +376,8 @@
sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}. Markup chunks start
with an empty sub-chunk, and a second empty sub-chunk indicates
close of an element. Any other non-empty chunk consists of plain
- text. For example, see \verb|~~/src/Pure/General/yxml.ML| or
- \verb|~~/src/Pure/General/yxml.scala|.
+ text. For example, see \verb|~~/src/Pure/PIDE/yxml.ML| or
+ \verb|~~/src/Pure/PIDE/yxml.scala|.
YXML documents may be detected quickly by checking that the first
two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.%