minor corrections to indexing; added thms_containing
authorpaulson
Fri, 18 Aug 1995 16:09:41 +0200
changeset 1233 2856f382f033
parent 1232 454eb424c223
child 1234 56ee5cc35510
minor corrections to indexing; added thms_containing in header
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}