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

Lawrence Paulson 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 mailing list