[isabelle-dev] AFP failures

Dmitriy Traytel 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.

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 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 <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
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




More information about the isabelle-dev mailing list