# HG changeset patch
# User paulson
# Date 808053315 -7200
# Node ID 35703accdf31930937667024df6938488535e2e8
# Parent  3d739c8e253604119b71677c252085c28828ef06
minor polishing of text on findI, etc.

diff -r 3d739c8e2536 -r 35703accdf31 doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Thu Aug 10 13:14:34 1995 +0200
+++ b/doc-src/Ref/goals.tex	Thu Aug 10 13:15:15 1995 +0200
@@ -165,8 +165,8 @@
 \index{theorems!retrieving}
 
 The following functions retrieve theorems (together with their names) from
-the theorem database. Hence they can only find theorems which have explicitly
-been stored in the database, using \ttindex{qed}, \ttindex{bind_thm} or
+the theorem database.  Hence they can only find theorems that have explicitly
+been stored in the database using \ttindex{qed}, \ttindex{bind_thm} or
 related functions.
 \begin{ttbox} 
 findI:         int -> (string * thm)list
@@ -175,22 +175,22 @@
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{findI} $i$]\index{assumptions!of main goal}
-  returns all ``introduction rules'' applicable to subgoal $i$, i.e.\ all
+  returns all ``introduction rules'' applicable to subgoal $i$ --- all
   theorems whose conclusion matches (rather than unifies with) subgoal
-  $i$. Useful in connection with {\tt resolve_tac}.
+  $i$.  Useful in connection with {\tt resolve_tac}.
 
 \item[\ttindexbold{findE} $n$ $i$] returns all ``elimination rules''
-  applicable to premise $n$ of subgoal $i$, i.e.\ all those theorems whose
-  first premise matches premise $n$ of subgoal $i$. Useful in connection with
+  applicable to premise $n$ of subgoal $i$ --- all those theorems whose
+  first premise matches premise $n$ of subgoal $i$.  Useful in connection with
   {\tt eresolve_tac} and {\tt dresolve_tac}.
 
 \item[\ttindexbold{findEs} $i$] returns all ``elimination rules'' applicable
-  to subgoal $i$, i.e.\ all those theorems whose first premise matches some
-  premise of subgoal $i$. Useful in connection with {\tt eresolve_tac} and
+  to subgoal $i$ --- all those theorems whose first premise matches some
+  premise of subgoal $i$.  Useful in connection with {\tt eresolve_tac} and
   {\tt dresolve_tac}.
 
-\item[\ttindexbold{thms_containing} $strings$] returns all theorems which
-  contain all of the constants in $strings$. Note that a few basic constants
+\item[\ttindexbold{thms_containing} $strings$] returns all theorems that
+  contain all of the constants in $strings$.  Note that a few basic constants
   like \verb$==>$ are ignored.
 \end{ttdescription}