Re: [isabelle-dev] Slow builds due to excessive heap images

2017-10-28 Thread Makarius
On 28/10/17 22:26, Makarius wrote: > We are presently testing Poly/ML 5.7.1 by default (see > Isabelle/aefaaef29c58) and there are already interesting performance > figures, e.g. see: > > http://isabelle.in.tum.de/devel/build_status > http://isabelle.in.tum.de/devel/build_status/Linux_A >

[isabelle-dev] Slow builds due to excessive heap images

2017-10-28 Thread Makarius
We are presently testing Poly/ML 5.7.1 by default (see Isabelle/aefaaef29c58) and there are already interesting performance figures, e.g. see: http://isabelle.in.tum.de/devel/build_status http://isabelle.in.tum.de/devel/build_status/Linux_A http://isabelle.in.tum.de/devel/build_status/AFP

Re: [isabelle-dev] linordered_semiring_1

2017-10-28 Thread Florian Haftmann
Hi Akihisa, thanks for pointing that out. I will take care of this. All the best, Florian Am 20.10.2017 um 17:37 schrieb Yamada, Akihisa: > Dear Isabelle/HOL developers, > > I propose to make linordered_semiring_1 a subclass of zero_less_one. > > class linordered_semiring_1 = >