--- 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%