--- a/doc-src/Ref/goals.tex Fri Aug 18 15:54:22 1995 +0200
+++ b/doc-src/Ref/goals.tex Fri Aug 18 16:09:41 1995 +0200
@@ -119,7 +119,7 @@
\subsection{Extracting and storing the proved theorem}
\label{ExtractingAndStoringTheProvedTheorem}
-\index{theorems!from subgoal module}
+\index{theorems!extracting proved}
\begin{ttbox}
result : unit -> thm
uresult : unit -> thm
@@ -169,9 +169,10 @@
been stored in the database using \ttindex{qed}, \ttindex{bind_thm} or
related functions.
\begin{ttbox}
-findI: int -> (string * thm)list
-findE: int -> int -> (string * thm)list
-findEs: int -> (string * thm)list
+findI : int -> (string * thm) list
+findE : int -> int -> (string * thm) list
+findEs : int -> (string * thm) list
+thms_containing : string list -> (string * thm) list
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{findI} $i$]\index{assumptions!of main goal}