diff -r c22b507e1407 -r e81ebb37aa83 CookBook/Recipes/Oracle.thy --- 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}