--- a/ProgTutorial/Recipes/Oracle.thy Fri Oct 29 13:16:45 2010 +0200
+++ b/ProgTutorial/Recipes/Oracle.thy Fri Oct 29 13:46:37 2010 +0200
@@ -19,7 +19,7 @@
\begin{readmore}
A short introduction to oracles can be found in [isar-ref: no suitable label
for section 3.11]. A simple example, which we will slightly extend here,
- is given in @{ML_file "FOL/ex/Iff_Oracle.thy"}. The raw interface for adding
+ is given in @{ML_file "HOL/ex/Iff_Oracle.thy"}. The raw interface for adding
oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm.ML"}.
\end{readmore}
@@ -152,4 +152,4 @@
*}
-end
\ No newline at end of file
+end