diff -r 3446d2b6a19f -r d9d2a0cadd5e doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Jun 15 09:01:15 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Jun 15 09:01:48 2005 +0200
@@ -153,6 +153,27 @@
 \isamarkuptrue%
 \isamarkupfalse%
 %
+\isamarkupsubsection{Variable names%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+It sometimes happens that you want to change the name of a
+variable in a theorem before printing it. This can easily be achieved
+with the help of Isabelle's instantiation attribute \texttt{where}:
+\isa{{\isasymlbrakk}{\isasymphi}{\isacharsemicolon}\ {\isasympsi}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isasymand}\ {\isasympsi}} is the result of
+\begin{quote}
+\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
+\end{quote}
+To support the ``\_''-notation for irrelevant variables
+the constant \texttt{DUMMY} has been introduced:
+\isa{fst\ {\isacharparenleft}a{\isacharcomma}\ \_{\isacharparenright}\ {\isacharequal}\ a} is produced by
+\begin{quote}
+\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
+\end{quote}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Inference rules%
 }
 \isamarkuptrue%