--- a/doc-src/System/Thy/Misc.thy Sun Nov 28 20:36:45 2010 +0100
+++ b/doc-src/System/Thy/Misc.thy Sun Nov 28 21:07:28 2010 +0100
@@ -219,7 +219,7 @@
text {*
Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's
object-logics as a model for your own developments. For example,
- see @{"file" "~~/src/FOL/IsaMakefile"}.
+ see @{file "~~/src/FOL/IsaMakefile"}.
*}
@@ -324,8 +324,8 @@
sub-chunks separated by @{text "\<^bold>Y"}. 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 @{"file" "~~/src/Pure/General/yxml.ML"} or
- @{"file" "~~/src/Pure/General/yxml.scala"}.
+ text. For example, see @{file "~~/src/Pure/General/yxml.ML"} or
+ @{file "~~/src/Pure/General/yxml.scala"}.
YXML documents may be detected quickly by checking that the first
two characters are @{text "\<^bold>X\<^bold>Y"}.