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.pope...@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, _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
