Hi all,
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
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
Of course we don’t have any formal curation policy for the library, but Zorn's
lemma is a fundamental result. Perhaps we need to think about what things are
and are not allowed in the library. Deleting things will always be risky.
Larry
On 26 Nov 2013, at 11:30, Johannes Hölzl hoe...@in.tum.de
Zorn is supposed to move to Main together with the new (co)datatype
package. I guess it was removed from Library only by mistake.
Dmitriy
Am 26.11.2013 12:58, schrieb Lawrence Paulson:
Of course we don’t have any formal curation policy for the library, but Zorn's
lemma is a fundamental
Am 26.11.2013 um 13:01 schrieb Dmitriy Traytel tray...@in.tum.de:
Zorn is supposed to move to Main together with the new (co)datatype package.
I guess it was removed from Library only by mistake.
Yes, it should definitely be in Library for now. My change 483131676087 took it
out by mistake.
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
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
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
On 26 Nov 2013, at 11:44 pm, Makarius makar...@sketis.net wrote:
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
