equal
deleted
inserted
replaced
933 Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem |
933 Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem |
934 depends upon oracle calls. |
934 depends upon oracle calls. |
935 |
935 |
936 \begin{ttbox} |
936 \begin{ttbox} |
937 invoke_oracle : theory * Sign.sg * exn -> thm |
937 invoke_oracle : theory * Sign.sg * exn -> thm |
938 set_oracle : Sign.sg -> typ -> string |
938 set_oracle : (Sign.sg * exn -> term) -> theory -> theory |
939 \end{ttbox} |
939 \end{ttbox} |
940 \begin{ttdescription} |
940 \begin{ttdescription} |
941 \item[\ttindexbold{invoke_oracle} ($thy$, $sign$, $exn$)] invokes the oracle |
941 \item[\ttindexbold{invoke_oracle} ($thy$, $sign$, $exn$)] invokes the oracle |
942 of theory $thy$ passing the information contained in the exception value |
942 of theory $thy$ passing the information contained in the exception value |
943 $exn$ and creating a theorem having signature $sign$. Errors arise if $thy$ |
943 $exn$ and creating a theorem having signature $sign$. Errors arise if $thy$ |