[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

@{thm [mode=Rule,show_types] Nat.induct [no_vars]}{\sc Ind-Nat}

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.