changeset 16396 d9d2a0cadd5e
parent 16176 ef83d8e097ba
child 17125 e6a82d1a1829
--- 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 @@
+\isamarkupsubsection{Variable names%
+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
+\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
+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
+\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
 \isamarkupsubsection{Inference rules%