[isabelle-dev] AFP failures

[Johannes Hölzl]

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.

 - Johannes