Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-28 Thread David Matthews
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,

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

2019-01-28 Thread Lawrence Paulson
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

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-28 Thread Bertram Felgenhauer
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