On Tue, 26 Nov 2013, Johannes Hölzl wrote:
Am Dienstag, den 26.11.2013, 11:52 +0100 schrieb Jasmin Christian
Blanchette:
The AFP tests are finally back, and this revealed a series of failures
related to my refactorings last week. Looking more closely at the
falures, I found they were all in the LaTeX generation, which I hadn't
tested locally before pushing. In most of the theories, it's the LaTeX
symbol \sqsubset that causes problem, because the necessary package is
not included.
Does anybody have any idea of why this suddenly pops up as an issue
just because I moved a few theories around?
Looks like Zorn's lemma is not included in HOL-Library anymore. When
Coinductive loads Zorn it is also included in the Latex document. (Zorn
uses \sqsubset in a local)
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?
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
