# HG changeset patch
# User paulson
# Date 813928186 -3600
# Node ID ea8b657a9c9209e33bcb82ec2b92b2ff28d03387
# Parent  92543c633f20571ae6c95bb2d903c0c2ffd6ed81
Documented store_thm and moved qed to top

diff -r 92543c633f20 -r ea8b657a9c92 doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Mon Oct 16 16:32:56 1995 +0100
+++ b/doc-src/Ref/goals.tex	Tue Oct 17 12:09:46 1995 +0100
@@ -121,12 +121,18 @@
 \label{ExtractingAndStoringTheProvedTheorem}
 \index{theorems!extracting proved}
 \begin{ttbox} 
+qed       : string -> unit
 result    : unit -> thm
 uresult   : unit -> thm
 bind_thm  : string * thm -> unit
-qed       : string -> unit
+store_thm : string * thm -> thm
 \end{ttbox}
 \begin{ttdescription}
+\item[\ttindexbold{qed} $name$] is the usual way of ending a proof.
+  It combines {\tt result} and {\tt bind_thm}: it gets the theorem using {\tt
+  result()} and stores it in Isabelle's theorem database.  See below for
+  details. 
+
 \item[\ttindexbold{result}()]\index{assumptions!of main goal}
   returns the final theorem, after converting the free variables to
   schematics.  It discharges the assumptions supplied to the matching 
@@ -149,15 +155,14 @@
   \ttindex{rewrite_tac}),\index{definitions!unfolding} or when
   \ttindex{assume_ax} has been used.
 
-\item[\ttindexbold{bind_thm}($name$, $thm$)]\index{theorems!storing of}
+\item[\ttindexbold{bind_thm}($name$, $thm$)]\index{theorems!storing}
   stores {\tt standard($thm$)} (see \S\ref{MiscellaneousForwardRules})
-  in Isabelle's theorem database and in the ML variable $name$. The
-  theorem can be retrieved from Isabelle's database by {\tt get_thm}
+  in Isabelle's theorem database and in the {\ML} variable $name$.  The
+  theorem can be retrieved from the database using {\tt get_thm}
   (see \S\ref{BasicOperationsOnTheories}).
 
-\item[\ttindexbold{qed} $name$]
-  combines {\tt result} and {\tt bind_thm} in that it first uses {\tt
-  result()} to get the theorem and then stores it like {\tt bind_thm}.
+\item[\ttindexbold{store_thm}($name$, $thm$)]\index{theorems!storing} stores
+  $thm$ in Isabelle's theorem database and returns that theorem.
 \end{ttdescription}
 
 
@@ -418,7 +423,7 @@
 
 \item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;]
 acts like {\tt prove_goal} but also stores the resulting theorem in
-Isabelle's theorem database and in the ML variable $name$ (see
+Isabelle's theorem database and in the {\ML} variable $name$ (see
 \S\ref{ExtractingAndStoringTheProvedTheorem}).
 
 \item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula}