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. *}