qed "";
authorwenzelm
Fri, 24 Sep 1999 12:22:49 +0200
changeset 75912d89d12f31eb
parent 7590 76c9e71d491a
child 7592 c29a222cf981
qed "";
doc-src/Ref/goals.tex
     1.1 --- a/doc-src/Ref/goals.tex	Thu Sep 23 19:22:52 1999 +0200
     1.2 +++ b/doc-src/Ref/goals.tex	Fri Sep 24 12:22:49 1999 +0200
     1.3 @@ -191,6 +191,10 @@
     1.4  
     1.5  \end{ttdescription}
     1.6  
     1.7 +The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be empty
     1.8 +(\texttt{""}) as well; in that case the result is \emph{not} stored, but
     1.9 +proper checks and presentation of the result still apply.
    1.10 +
    1.11  
    1.12  \subsection{Extracting axioms and stored theorems}
    1.13  \index{theories!axioms of}\index{axioms!extracting}