doc-src/Ref/goals.tex
changeset 7990 0a604b2fc2b1
parent 7805 0ae9ddc36fe0
child 8136 8c65f3ca13f2
     1.1 --- a/doc-src/Ref/goals.tex	Sun Oct 31 15:26:37 1999 +0100
     1.2 +++ b/doc-src/Ref/goals.tex	Sun Oct 31 20:11:23 1999 +0100
     1.3 @@ -186,14 +186,14 @@
     1.4    stores $thm$ in the theorem database associated with its theory and
     1.5    returns that theorem.
     1.6    
     1.7 -\item[\ttindexbold{bind_thms} and \ttindexbold{store_thms}] are similar to
     1.8 +\item[\ttindexbold{bind_thms} \textrm{and} \ttindexbold{store_thms}] are similar to
     1.9    \texttt{bind_thm} and \texttt{store_thm}, but store lists of theorems.
    1.10  
    1.11  \end{ttdescription}
    1.12  
    1.13 -The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be empty
    1.14 -(\texttt{""}) as well; in that case the result is \emph{not} stored, but
    1.15 -proper checks and presentation of the result still apply.
    1.16 +The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be the empty
    1.17 +string as well; in that case the result is \emph{not} stored, but proper
    1.18 +checks and presentation of the result still apply.
    1.19  
    1.20  
    1.21  \subsection{Extracting axioms and stored theorems}