--- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Nov 29 11:22:40 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Nov 29 11:27:39 2010 +0100
@@ -1203,7 +1203,7 @@
\end{description}
- 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
+ See \verb|~~/src/HOL/ex/Iff_Oracle.thy| for a worked example of
defining a new primitive rule as oracle, and turning it into a proof
method.%
\end{isamarkuptext}%