On Tue, 18 Mar 2014, Brian Huffman wrote:
Revision c7dfd924a165 should now take care of it.
Thanks. Now the spice can flow again ...
Are you actually working together with Johannes Hölzl on these parts, or
is your later change 32b7eafc5a52 merely a coincidence?
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.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
