Re: [isabelle] property of infinite cardinals

Andrei Popescu wrote:
> (At least for well-ordered 'a should be provable.  Related question: can one prove (similarly to the case of ZF+Choice) that any type can be well-ordered?

Yes. See Library/Zorn.thy

> Is there any theory of ordinals developed in Isabelle/HOL?)

Yes. See


> Thank you in advance, 
>    Andrei Popescu 

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.