diff -r edcdecd55655 -r c4336e45f199 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Thu Oct 28 22:23:11 2010 +0200 +++ b/doc-src/IsarRef/Thy/Spec.thy Thu Oct 28 22:39:59 2010 +0200 @@ -1159,7 +1159,7 @@ \end{description} - See @{"file" "~~/src/FOL/ex/Iff_Oracle.thy"} for a worked example of + See @{"file" "~~/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. *}