--- a/doc-src/Ref/theories.tex Thu Feb 05 10:26:16 1998 +0100
+++ b/doc-src/Ref/theories.tex Thu Feb 05 10:26:59 1998 +0100
@@ -838,7 +838,8 @@
\begin{ttbox}
invoke_oracle : theory -> xstring -> Sign.sg * object -> thm
-Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory -> theory
+Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory
+ -> theory
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)]
@@ -914,8 +915,8 @@
Now in \texttt{IffOracle.ML} we first define a wrapper for invoking
the oracle:
\begin{ttbox}
-fun iff_oracle n =
- invoke_oracle IffOracle.thy "iff" (sign_of IffOracle.thy, IffOracleExn n);
+fun iff_oracle n = invoke_oracle IffOracle.thy "iff"
+ (sign_of IffOracle.thy, IffOracleExn n);
\end{ttbox}
Here are some example applications of the \texttt{iff} oracle. An