CookBook/Recipes/Oracle.thy
changeset 154 e81ebb37aa83
parent 120 c39f83d8daeb
child 181 5baaabe1ab92
--- 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}