Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] document generation for selected theories only

view this post on Zulip Email Gateway (Aug 22 2022 at 10:45):

From: Gergely Buday <gbuday@gmail.com>
Hi,

I have a ROOT file that specifies

theories [ document = true ]

"MyTheory.thy"

As I understand if I import other theories and there are ROOT files
belonging to them they will be processed as well for document preparation.

To not enable this I can give a section

theories [document = false ]

but that sometimes make a long list.

Is it possible to select theories and produce the proof document _only_ for
them?

view this post on Zulip Email Gateway (Aug 22 2022 at 11:08):

From: Makarius <makarius@sketis.net>
You can \input the generated theory document nodes in the root.tex --
instead of the \input{session} that is there by default.

Makarius

Last updated: Apr 25 2024 at 08:20 UTC