Corrected typo regarding the type of set_oracle
authorpaulson
Tue, 23 Jul 1996 13:19:27 +0200
changeset 1880 78c4b3ddba6c
parent 1879 83c70ad381c1
child 1881 5b297e9ec3fc
Corrected typo regarding the type of set_oracle
doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Mon Jul 22 16:24:47 1996 +0200
+++ b/doc-src/Ref/theories.tex	Tue Jul 23 13:19:27 1996 +0200
@@ -935,7 +935,7 @@
 
 \begin{ttbox}
      invoke_oracle : theory * Sign.sg * exn -> thm
-     set_oracle    : Sign.sg -> typ -> string
+     set_oracle    : (Sign.sg * exn -> term) -> theory -> theory
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{invoke_oracle} ($thy$, $sign$, $exn$)] invokes the oracle