On Tue, 26 Nov 2013, Johannes Hölzl wrote:
Am Dienstag, den 26.11.2013, 13:12 +0100 schrieb Makarius:
[..]
I added now Zorn to HOL-Library (isa# acb41098607a), at least
Coinductive works now.
I don't understand this at all, neither the above explanation nor the
formal changeset (with its vacuous log message).
How does the inclusion or non-inclusion of some theory affect the latex
macro environment?
When Zorn is not in HOL-Library its tex-output is included in the
document for AFP-Coinductive. The root.tex for AFP-Coinductive does not
include the setup for \sqsubset, so its pdf-generation fails. By adding
Zorn back to HOL-Library, the output for Zorn is not included in the pdf
for AFP-Coinductive.
This means, by rearranging certain library sessions, AFP documents
suddenly include theories into the document that are not meant to be
there. We don't have a systematic check for this, so AFP documents are
generally endangered. It was merely a fortunate accident that the
additional Zorn.tex of AFP/Coinductive was using undefined latex macros.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
