Re: [isabelle] Influence order of theories in an Isabelle document?



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

On 12/10/2019 21:53, Eugene W. Stark wrote:
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.


On 10/12/19 2:41 PM, Eugene W. Stark wrote:
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.









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.