<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class="">The recent failure in Multivariable_Analysis was caused by the \nexists macro, which is not defined:</div><div class=""><br class="">! Undefined control sequence.<br class=""><recently read> \nexists <br class=""></div><div class=""><br class=""></div><div class="">The corresponding source line is here:</div><div class=""><br class=""></div>Multivariate_Analysis/Brouwer_Fixpoint.thy:    have nog: "\<nexists>g. continuous_on (S \<union> connected_component_set (- S) a) g \<and><br class=""><br class=""><div class="">What’s unfortunate is that the “negated exists” quantifier is available both for input and output in Isabelle, just not as a TeX macro.</div><div class=""><br class=""></div><div class="">I’ve pushed a fix. However, ideally this macro should be defined somehow and my change reverted.</div><div class=""><br class=""></div><div class="">Larry<br class=""></div><img height="286" width="444" apple-width="yes" apple-height="yes" apple-inline="yes" id="DB5360A9-C1A8-4CB3-ADB0-4D841BC7D54F" src="cid:03261917-67C8-4622-B275-9E204DECE002@cl.cam.ac.uk" class=""></body></html>