Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [ExternalEmail] Unwanted dependency documents ...

view this post on Zulip Email Gateway (Aug 22 2022 at 15:05):

From: Gerwin.Klein@data61.csiro.au
In fact, if you are building on existing AFP entries, you should of course re-use their session images. You can’t merge sessions, so we need to pick one, e.g.:

chapter AFP

session Parity_Game_Base (AFP) = Coinductive +
options [timeout = 600]
theories [document = false]
"../Graph_Theory/Digraph_Isomorphism"

session Parity_Game (AFP) = Parity_Game_Base +
options [timeout = 600]
theories
PositionalDeterminacy
AttractorInductive
Graph_TheoryCompatibility
document_files
"root.tex"
“root.bib"

Cheers,
Gerwin

Last updated: Apr 26 2024 at 08:19 UTC