Email Gateway (Aug 19 2022 at 15:12): Email Gateway (Aug 19 2022 at 15:12):From: Gergely Buday <gbuday@gmail.com>
Hi,
is it possible to typeset one subgoal per line as it appears in Isabelle/JEdit?
I used
isabelle build -D .
Email Gateway (Aug 19 2022 at 16:57):From: Gergely Buday <gbuday@gmail.com>
Hi,
when I use the @{subgoals} antiquotation, the subgoals come continuously in
the generated pdf as there are no linebreaks in between them.
At what part of the Isabelle code I could hack to emit "\\ " into the
generated latex file?
Email Gateway (Aug 19 2022 at 16:57):From: Makarius <makarius@sketis.net>
On Fri, 16 Jan 2015, Gergely Buday wrote:
when I use the @{subgoals} antiquotation, the subgoals come continuously
in the generated pdf as there are no linebreaks in between them.At what part of the Isabelle code I could hack to emit "\\ " into the
generated latex file?
Instead of "hacking" it is better to read the manual: isar-ref section
Last updated: Apr 16 2024 at 16:19 UTC