'Iff_Oracle.thy' has moved
authorgriff
Fri, 29 Oct 2010 13:46:37 +0200
changeset 457 aedfdcae39a9
parent 456 89fccd3d5055
child 458 242e81f4d461
'Iff_Oracle.thy' has moved
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