Email Gateway (Aug 18 2022 at 18:13): Email Gateway (Aug 18 2022 at 18:13):From: Alfio Martini <alfio.martini@acm.org>
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
Email Gateway (Aug 18 2022 at 18:13):From: Alfio Martini <alfio.martini@acm.org>
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@acm.org>
Date: Wed, Aug 17, 2011 at 11:51 AM
Subject: Renaming names of arbitrary values in document preparation
To: isabelle-users@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
Last updated: Apr 23 2024 at 12:29 UTC