summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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.

--- 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}