[isabelle-dev] cardinality primitives in Isabelle/HOL?
lp15 at cam.ac.uk
Mon Jan 28 12:13:51 CET 2019
Last January 24, I moved Fpow into Main and introduced Library/Equipollence.thy. Hope you like it.
> 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,
More information about the isabelle-dev