1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 29 11:22:40 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 29 11:27:39 2010 +0100
     1.3 @@ -1203,7 +1203,7 @@
     1.4  
     1.5    \end{description}
     1.6  
     1.7 -  See \hyperlink{file.~~/src/HOL/ex/Iff-Oracle.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}}Iff{\isaliteral{5F}{\isacharunderscore}}Oracle{\isaliteral{2E}{\isachardot}}thy}}}} for a worked example of
     1.8 +  See \verb|~~/src/HOL/ex/Iff_Oracle.thy| for a worked example of
     1.9    defining a new primitive rule as oracle, and turning it into a proof
    1.10    method.%
    1.11  \end{isamarkuptext}%