# HG changeset patch
# User wenzelm
# Date 938168569 -7200
# Node ID 2d89d12f31eb58f17f653dfc97a554b6c360b0b8
# Parent  76c9e71d491a6359d147939f04a4eb1bb34174a8
qed "";

diff -r 76c9e71d491a -r 2d89d12f31eb doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Thu Sep 23 19:22:52 1999 +0200
+++ b/doc-src/Ref/goals.tex	Fri Sep 24 12:22:49 1999 +0200
@@ -191,6 +191,10 @@
 
 \end{ttdescription}
 
+The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be empty
+(\texttt{""}) as well; in that case the result is \emph{not} stored, but
+proper checks and presentation of the result still apply.
+
 
 \subsection{Extracting axioms and stored theorems}
 \index{theories!axioms of}\index{axioms!extracting}