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