--- a/CookBook/Recipes/Oracle.thy Sat Feb 28 14:18:02 2009 +0000
+++ b/CookBook/Recipes/Oracle.thy Sun Mar 01 21:48:59 2009 +0000
@@ -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/IffOracle.thy"}. The raw interface for adding
+ is given in @{ML_file "FOL/ex/Iff_Oracle.thy"}. The raw interface for adding
oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm.ML"}.
\end{readmore}