[isabelle-dev] HOL-Multivariate-Analysis [was: HOL-Decision_Procs FAILED]

[Florian Haftmann]

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

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140318/53da9f69/attachment.sig>