On 28/01/2019 09:20, Bertram Felgenhauer wrote:
I've made sure that the machine is mostly idle; things will be much
different if several processes start competing for the ressources.
I intended to experiment with smaller numbers but have not yet done so.
On another, similar machine,
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 wrote:
>
> Sorry for my late reply. I agree it makes sense to move such basic operators
> (and facts) into Main. The Ordinals and Cardinals
Makarius wrote:
> There was indeed something odd with sharing: David Matthews has changed
> that in polyml-1b2dcf8f5202 (see Isabelle/bb0a354f6b46).
I may give it another try later...
> > Hardware:
> > i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD
> >
> > Common build