Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] @{subgoals}

view this post on Zulip 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 .

view this post on Zulip 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?

view this post on Zulip 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: Nov 21 2024 at 12:39 UTC