--- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Feb 16 20:23:43 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Feb 16 20:25:21 2009 +0100
@@ -1196,7 +1196,7 @@
\end{description}
- See \hyperlink{file.~~/src/FOL/ex/IffOracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}IffOracle{\isachardot}thy}}}} for a worked example of
+ See \hyperlink{file.~~/src/FOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of
defining a new primitive rule as oracle, and turning it into a proof
method.%
\end{isamarkuptext}%