Email Gateway (Aug 22 2022 at 20:44): Email Gateway (Aug 22 2022 at 20:44):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Apologies if I have missed this in the documentation, but is there a way to influence
the order in which theories within a session are presented in an Isabelle document?
I am willing to tolerate the theories being presented in dependency order, but within
that constraint I would like to keep logically related theories together, rather than
having them merged using some random topological sort. Thanks for any help.
Email Gateway (Aug 22 2022 at 20:44):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Never mind, I suppose the answer is to substitute one's own LaTeX code in root.tex,
rather than inputting the generated session.tex file. It wasn't occurring to me to
muck with the generated files. Sorry for the spam.
Email Gateway (Aug 22 2022 at 20:44):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Eugene,
You can specify the order in the ROOT file. If you just list the leaves of the theory
dependency graph, then the imported theory will show up in some random topological sort of
dependency order. By specifying intermediate theories, you can pin down that order. Note,
however, that you cannot get an order that would be in conflict with the dependencies.
Hope this helps,
Andreas
Last updated: Apr 25 2024 at 01:08 UTC