# HG changeset patch
# User griff
# Date 1288352797 -7200
# Node ID aedfdcae39a9520d3172650f6445a147403d574a
# Parent  89fccd3d50556c6064bc783f3dae0604d09ac07c
'Iff_Oracle.thy' has moved

diff -r 89fccd3d5055 -r aedfdcae39a9 ProgTutorial/Recipes/Oracle.thy
--- 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