[isabelle-dev] HOL-Multivariate-Analysis [was: HOL-Decision_Procs FAILED]
florian.haftmann at informatik.tu-muenchen.de
Tue Mar 18 22:08:55 CET 2014
> Did you notice practically relevant performance issues with the
> HOL-Multivariate-Analysis sessions? It is one of the (relatively few)
> sessions where the fact name space change (for semantic completion) has
> significant impact. I am still reading the tea leaves in the charts at
> http://isabelle.in.tum.de/devel/. It is not yet clear to me, why this
> session suffers more than others.
I am currently also doing some work on Inf/Sup/INF/SUP, which is very
prominent in HOL-Multivariate-Analysis. I still have two intermediate
steps in front me of before tackling the issue I want to get done
finally. The present intermediate step is not as polished as it could
be. But there should not be a overall performance impact.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 263 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev