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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
