diff -r 6cfacec435e6 -r 3cd23f676c5b doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 29 11:22:40 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 29 11:27:39 2010 +0100
@@ -897,7 +897,7 @@
   The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
   \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
   applications in confluence theory, lattice theory and projective
-  geometry.  See \hyperlink{file.~~/src/HOL/ex/Coherent.thy}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}HOL{\isaliteral{2F}{\isacharslash}}ex{\isaliteral{2F}{\isacharslash}}Coherent{\isaliteral{2E}{\isachardot}}thy}}}} for some
+  geometry.  See \verb|~~/src/HOL/ex/Coherent.thy| for some
   examples.%
 \end{isamarkuptext}%
 \isamarkuptrue%