# HG changeset patch
# User paulson
# Date 808754981 -7200
# Node ID 2856f382f033a028e49568714cc15f756dacd0f7
# Parent  454eb424c2230d17033e16773faf81cbd045d361
minor corrections to indexing; added thms_containing
in header

diff -r 454eb424c223 -r 2856f382f033 doc-src/Ref/goals.tex
--- 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}