[isabelle] Renaming names of arbitrary values in document preparation (Answer)



Dear Isabelle Users,

Looking again at LaTeXsugar, I found how to do it. It´s been always there,
right
in front of my nose. So  what I wanted is something like:

\begin{center}
@{thm [mode=Rule,show_types] Nat.induct [where Nat = n,no_vars,rename_abs
x0]}{\sc Ind-Nat}
\end{center}

Best!!

---------- Forwarded message ----------
From: Alfio Martini <alfio.martini at acm.org>
Date: Wed, Aug 17, 2011 at 11:51 AM
Subject: Renaming names of arbitrary values in document preparation
To: isabelle-users at cl.cam.ac.uk


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



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