doc-src/IsarRef/Thy/Spec.thy
changeset 40239 c4336e45f199
parent 40079 07445603208a
child 40240 a2dde53b15ef
--- 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.
 *}