qed "";

--- 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}