# HG changeset patch
# User krauss
# Date 1271260222 -7200
# Node ID 1faa0fc3417477c381ef6d43c50377589acd8bd0
# Parent  0be811a98d3ab3cbedba2fbf057269cc8d834735
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.

diff -r 0be811a98d3a -r 1faa0fc34174 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Apr 14 16:15:19 2010 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Apr 14 17:50:22 2010 +0200
@@ -174,6 +174,14 @@
 \begin{quote}
 \verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
 \end{quote}
+Variables that are bound by quantifiers or lambdas cannot be renamed
+like this. Instead, the attribute \texttt{rename\_abs} does the
+job. It expects a list of names or underscores, similar to the
+\texttt{of} attribute:
+\begin{quote}
+\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
+\end{quote}
+produces @{thm split_paired_All[rename_abs _ l r]}.
 *}
 
 subsection "Inference rules"
diff -r 0be811a98d3a -r 1faa0fc34174 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Apr 14 16:15:19 2010 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Apr 14 17:50:22 2010 +0200
@@ -233,7 +233,15 @@
 \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ \_{\isacharparenright}\ {\isacharequal}\ a} is produced by
 \begin{quote}
 \verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
-\end{quote}%
+\end{quote}
+Variables that are bound by quantifiers or lambdas cannot be renamed
+like this. Instead, the attribute \texttt{rename\_abs} does the
+job. It expects a list of names or underscores, similar to the
+\texttt{of} attribute:
+\begin{quote}
+\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
+\end{quote}
+produces \isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}l\ r{\isachardot}\ P\ {\isacharparenleft}l{\isacharcomma}\ r{\isacharparenright}{\isacharparenright}}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %