author paulson Thu, 10 Aug 1995 13:15:15 +0200 changeset 1225 35703accdf31 parent 1224 3d739c8e2536 child 1226 e9c01f251f5d
minor polishing of text on findI, etc.
 doc-src/Ref/goals.tex file | annotate | diff | comparison | revisions
--- 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}