[isabelle-dev] cardinality primitives in Isabelle/HOL?

[Lawrence Paulson]

Last January 24, I moved Fpow into Main and introduced Library/Equipollence.thy. Hope you like it.

Larry

> On 26 Jan 2019, at 15:14, Andrei Popescu <A.Popescu at mdx.ac.uk> wrote:
> 
> Sorry for my late reply. I agree it makes sense to move such basic operators (and facts) into Main. The Ordinals and Cardinals development was "destined" to this sort of exports from the very beginning.    
> 
> Best wishes,