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 <> 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

Reply via email to