updated file locations;
authorwenzelm
Wed Sep 07 18:01:01 2011 +0200 (2011-09-07)
changeset 447991fd0a1276a09
parent 44798 9900c0069ae6
child 44800 0472f2367efb
updated file locations;
doc-src/System/Thy/Misc.thy
doc-src/System/Thy/document/Misc.tex
     1.1 --- a/doc-src/System/Thy/Misc.thy	Wed Sep 07 17:42:57 2011 +0200
     1.2 +++ b/doc-src/System/Thy/Misc.thy	Wed Sep 07 18:01:01 2011 +0200
     1.3 @@ -336,8 +336,8 @@
     1.4    sub-chunks separated by @{text "\<^bold>Y"}.  Markup chunks start
     1.5    with an empty sub-chunk, and a second empty sub-chunk indicates
     1.6    close of an element.  Any other non-empty chunk consists of plain
     1.7 -  text.  For example, see @{file "~~/src/Pure/General/yxml.ML"} or
     1.8 -  @{file "~~/src/Pure/General/yxml.scala"}.
     1.9 +  text.  For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or
    1.10 +  @{file "~~/src/Pure/PIDE/yxml.scala"}.
    1.11  
    1.12    YXML documents may be detected quickly by checking that the first
    1.13    two characters are @{text "\<^bold>X\<^bold>Y"}.
     2.1 --- a/doc-src/System/Thy/document/Misc.tex	Wed Sep 07 17:42:57 2011 +0200
     2.2 +++ b/doc-src/System/Thy/document/Misc.tex	Wed Sep 07 18:01:01 2011 +0200
     2.3 @@ -376,8 +376,8 @@
     2.4    sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.  Markup chunks start
     2.5    with an empty sub-chunk, and a second empty sub-chunk indicates
     2.6    close of an element.  Any other non-empty chunk consists of plain
     2.7 -  text.  For example, see \verb|~~/src/Pure/General/yxml.ML| or
     2.8 -  \verb|~~/src/Pure/General/yxml.scala|.
     2.9 +  text.  For example, see \verb|~~/src/Pure/PIDE/yxml.ML| or
    2.10 +  \verb|~~/src/Pure/PIDE/yxml.scala|.
    2.11  
    2.12    YXML documents may be detected quickly by checking that the first
    2.13    two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.%