# HG changeset patch
# User wenzelm
# Date 936213661 -7200
# Node ID 0577bb18b1abc15346b409d893d05278bd5b370e
# Parent  cba45c114f3be28a882b734ac531858a59d84785
added bind_thms, store_thms;

diff -r cba45c114f3b -r 0577bb18b1ab doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Wed Sep 01 21:20:04 1999 +0200
+++ b/doc-src/Ref/goals.tex	Wed Sep 01 21:21:01 1999 +0200
@@ -134,11 +134,13 @@
 \label{ExtractingAndStoringTheProvedTheorem}
 \index{theorems!extracting proved}
 \begin{ttbox} 
-qed       : string -> unit
-result    : unit -> thm
-uresult   : unit -> thm
-bind_thm  : string * thm -> unit
-store_thm : string * thm -> thm
+qed        : string -> unit
+result     : unit -> thm
+uresult    : unit -> thm
+bind_thm   : string * thm -> unit
+bind_thms  : string * thm list -> unit
+store_thm  : string * thm -> thm
+store_thms : string * thm list -> thm list
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{qed} $name$;] is the usual way of ending a proof.
@@ -177,6 +179,10 @@
 \item[\ttindexbold{store_thm} ($name$, $thm$)]\index{theorems!storing}
   stores $thm$ in the theorem database associated with its theory and
   returns that theorem.
+  
+\item[\ttindexbold{bind_thms} and \ttindexbold{store_thms}] are similar to
+  \texttt{bind_thm} and \texttt{store_thm}, but store lists of theorems.
+
 \end{ttdescription}