1.1 --- a/doc-src/Ref/goals.tex	Mon Oct 16 16:32:56 1995 +0100
     1.2 +++ b/doc-src/Ref/goals.tex	Tue Oct 17 12:09:46 1995 +0100
     1.3 @@ -121,12 +121,18 @@
     1.4  \label{ExtractingAndStoringTheProvedTheorem}
     1.5  \index{theorems!extracting proved}
     1.6  \begin{ttbox} 
     1.7 +qed       : string -> unit
     1.8  result    : unit -> thm
     1.9  uresult   : unit -> thm
    1.10  bind_thm  : string * thm -> unit
    1.11 -qed       : string -> unit
    1.12 +store_thm : string * thm -> thm
    1.13  \end{ttbox}
    1.14  \begin{ttdescription}
    1.15 +\item[\ttindexbold{qed} $name$] is the usual way of ending a proof.
    1.16 +  It combines {\tt result} and {\tt bind_thm}: it gets the theorem using {\tt
    1.17 +  result()} and stores it in Isabelle's theorem database.  See below for
    1.18 +  details. 
    1.19 +
    1.20  \item[\ttindexbold{result}()]\index{assumptions!of main goal}
    1.21    returns the final theorem, after converting the free variables to
    1.22    schematics.  It discharges the assumptions supplied to the matching 
    1.23 @@ -149,15 +155,14 @@
    1.24    \ttindex{rewrite_tac}),\index{definitions!unfolding} or when
    1.25    \ttindex{assume_ax} has been used.
    1.26  
    1.27 -\item[\ttindexbold{bind_thm}($name$, $thm$)]\index{theorems!storing of}
    1.28 +\item[\ttindexbold{bind_thm}($name$, $thm$)]\index{theorems!storing}
    1.29    stores {\tt standard($thm$)} (see \S\ref{MiscellaneousForwardRules})
    1.30 -  in Isabelle's theorem database and in the ML variable $name$. The
    1.31 -  theorem can be retrieved from Isabelle's database by {\tt get_thm}
    1.32 +  in Isabelle's theorem database and in the {\ML} variable $name$.  The
    1.33 +  theorem can be retrieved from the database using {\tt get_thm}
    1.34    (see \S\ref{BasicOperationsOnTheories}).
    1.35  
    1.36 -\item[\ttindexbold{qed} $name$]
    1.37 -  combines {\tt result} and {\tt bind_thm} in that it first uses {\tt
    1.38 -  result()} to get the theorem and then stores it like {\tt bind_thm}.
    1.39 +\item[\ttindexbold{store_thm}($name$, $thm$)]\index{theorems!storing} stores
    1.40 +  $thm$ in Isabelle's theorem database and returns that theorem.
    1.41  \end{ttdescription}
    1.42  
    1.43  
    1.44 @@ -418,7 +423,7 @@
    1.45  
    1.46  \item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;]
    1.47  acts like {\tt prove_goal} but also stores the resulting theorem in
    1.48 -Isabelle's theorem database and in the ML variable $name$ (see
    1.49 +Isabelle's theorem database and in the {\ML} variable $name$ (see
    1.50  \S\ref{ExtractingAndStoringTheProvedTheorem}).
    1.51  
    1.52  \item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula}