[isabelle-dev] HOL-Decision_Procs FAILED

[Makarius]

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