# HG changeset patch
# User wenzelm
# Date 1234812321 -3600
# Node ID 2203ef9b55ce41678e1f6ce2c01e25eb4cd73285
# Parent  a9fc00f1b8f0d08a8bbdac277dc737bbc6747c51
updated generated files;

diff -r a9fc00f1b8f0 -r 2203ef9b55ce doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Feb 16 20:23:43 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Feb 16 20:25:21 2009 +0100
@@ -1196,7 +1196,7 @@
 
   \end{description}
 
-  See \hyperlink{file.~~/src/FOL/ex/IffOracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}IffOracle{\isachardot}thy}}}} for a worked example of
+  See \hyperlink{file.~~/src/FOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of
   defining a new primitive rule as oracle, and turning it into a proof
   method.%
 \end{isamarkuptext}%