1.1 --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Jun 15 09:01:15 2005 +0200
     1.2 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Jun 15 09:01:48 2005 +0200
     1.3 @@ -153,6 +153,27 @@
     1.4  \isamarkuptrue%
     1.5  \isamarkupfalse%
     1.6  %
     1.7 +\isamarkupsubsection{Variable names%
     1.8 +}
     1.9 +\isamarkuptrue%
    1.10 +%
    1.11 +\begin{isamarkuptext}%
    1.12 +It sometimes happens that you want to change the name of a
    1.13 +variable in a theorem before printing it. This can easily be achieved
    1.14 +with the help of Isabelle's instantiation attribute \texttt{where}:
    1.15 +\isa{{\isasymlbrakk}{\isasymphi}{\isacharsemicolon}\ {\isasympsi}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isasymand}\ {\isasympsi}} is the result of
    1.16 +\begin{quote}
    1.17 +\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
    1.18 +\end{quote}
    1.19 +To support the ``\_''-notation for irrelevant variables
    1.20 +the constant \texttt{DUMMY} has been introduced:
    1.21 +\isa{fst\ {\isacharparenleft}a{\isacharcomma}\ \_{\isacharparenright}\ {\isacharequal}\ a} is produced by
    1.22 +\begin{quote}
    1.23 +\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
    1.24 +\end{quote}%
    1.25 +\end{isamarkuptext}%
    1.26 +\isamarkuptrue%
    1.27 +%
    1.28  \isamarkupsubsection{Inference rules%
    1.29  }
    1.30  \isamarkuptrue%