# [isabelle] Renaming names of arbitrary values in document preparation

Dear Isabelle Users,
Assuming the context of the declaration
datatype Nat = Z | suc Nat
the following antiquotation command produces a very nicely typeset inference
rule:
\begin{center}
@{thm [mode=Rule,show_types] Nat.induct [no_vars]}{\sc Ind-Nat}
\end{center}
However, Isabelle chooses the same name (in this case /\ Nat) for the bound
variable in the rule. In proof mode
one can rename such choices using the rename_tac command. Unfortunately I
did not find how to do it in the
above. Took a careful look at chapter 4 of Isabelle reference manual (and
LaTex sugar too)
but I did not guess the way to do it.
Hope it is possible.
Many thanks
--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Porto Alegre - RS - Brasil

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*