[isabelle-dev] AFP failures
traytel at in.tum.de
Tue Nov 26 13:01:39 CET 2013
Zorn is supposed to move to Main together with the new (co)datatype
package. I guess it was removed from Library only by mistake.
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 result. Perhaps we need to think about what things are and are not allowed in the library. Deleting things will always be risky.
> On 26 Nov 2013, at 11:30, Johannes Hölzl <hoelzl at in.tum.de> wrote:
>> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev