1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 29 11:22:40 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 29 11:27:39 2010 +0100
     1.3 @@ -897,7 +897,7 @@
     1.4    The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
     1.5    \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
     1.6    applications in confluence theory, lattice theory and projective
     1.7 -  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
     1.8 +  geometry.  See \verb|~~/src/HOL/ex/Coherent.thy| for some
     1.9    examples.%
    1.10  \end{isamarkuptext}%
    1.11  \isamarkuptrue%