equal
deleted
inserted
replaced
172 the constant \texttt{DUMMY} has been introduced: |
172 the constant \texttt{DUMMY} has been introduced: |
173 @{thm fst_conv[where b = DUMMY]} is produced by |
173 @{thm fst_conv[where b = DUMMY]} is produced by |
174 \begin{quote} |
174 \begin{quote} |
175 \verb!@!\verb!{thm fst_conv[where b = DUMMY]}! |
175 \verb!@!\verb!{thm fst_conv[where b = DUMMY]}! |
176 \end{quote} |
176 \end{quote} |
|
177 Variables that are bound by quantifiers or lambdas cannot be renamed |
|
178 like this. Instead, the attribute \texttt{rename\_abs} does the |
|
179 job. It expects a list of names or underscores, similar to the |
|
180 \texttt{of} attribute: |
|
181 \begin{quote} |
|
182 \verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}! |
|
183 \end{quote} |
|
184 produces @{thm split_paired_All[rename_abs _ l r]}. |
177 *} |
185 *} |
178 |
186 |
179 subsection "Inference rules" |
187 subsection "Inference rules" |
180 |
188 |
181 text{* To print theorems as inference rules you need to include Didier |
189 text{* To print theorems as inference rules you need to include Didier |