1.1 --- a/doc-src/Ref/theories.tex	Wed Jan 18 11:36:04 1995 +0100
     1.2 +++ b/doc-src/Ref/theories.tex	Thu Jan 19 16:05:21 1995 +0100
     1.3 @@ -308,7 +308,7 @@
     1.4  
     1.5  
     1.6  
     1.7 -\section{Basic operations on theories}
     1.8 +\section{Basic operations on theories}\label{BasicOperationsOnTheories}
     1.9  \subsection{Extracting an axiom or theorem from a theory}
    1.10  \index{theories!axioms of}\index{axioms!extracting}
    1.11  \index{theories!theorems of}\index{theorems!extracting}
    1.12 @@ -319,12 +319,14 @@
    1.13  \end{ttbox}
    1.14  \begin{ttdescription}
    1.15  \item[\ttindexbold{get_axiom} $thy$ $name$]
    1.16 -returns an axiom with the given $name$ from $thy$, raising exception
    1.17 -\xdx{THEORY} if none exists.  Merging theories can cause several axioms
    1.18 -to have the same name; {\tt get_axiom} returns an arbitrary one.
    1.19 +  returns an axiom with the given $name$ from $thy$, raising exception
    1.20 +  \xdx{THEORY} if none exists.  Merging theories can cause several axioms
    1.21 +  to have the same name; {\tt get_axiom} returns an arbitrary one.
    1.22  
    1.23  \item[\ttindexbold{get_thm} $thy$ $name$]
    1.24 -  is analogous to {\tt get_axiom}, but looks for a stored theorem.
    1.25 +  is analogous to {\tt get_axiom}, but looks for a stored theorem. Like
    1.26 +  {\tt get_axiom} it searches all parents of a theory if the theorem
    1.27 +  is not associated with $thy$.
    1.28  
    1.29  \item[\ttindexbold{assume_ax} $thy$ $formula$]
    1.30    reads the {\it formula} using the syntax of $thy$, following the same
    1.31 @@ -427,7 +429,7 @@
    1.32  returns the additional axioms of the most recent extend node of~$thy$.
    1.33  
    1.34  \item[\ttindexbold{thms_of} $thy$]
    1.35 -similar to {\tt axioms_of}, but returns the stored theorems.
    1.36 +returns all theorems that are associated with $thy$.
    1.37  
    1.38  \item[\ttindexbold{parents_of} $thy$]
    1.39  returns the direct ancestors of~$thy$.