[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.