author | paulson |
Tue, 23 Jul 1996 13:19:27 +0200 | |
changeset 1880 | 78c4b3ddba6c |
parent 1879 | 83c70ad381c1 |
child 1881 | 5b297e9ec3fc |
--- 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