ProgTutorial/Recipes/Oracle.thy
changeset 457 aedfdcae39a9
parent 346 0fea8b7a14a1
child 517 d8c376662bb4
--- 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