The recent failure in Multivariable_Analysis was caused by the \nexists macro, 
which is not defined:

! Undefined control sequence.
<recently read> \nexists 

The corresponding source line is here:

Multivariate_Analysis/Brouwer_Fixpoint.thy:    have nog: "\<nexists>g. 
continuous_on (S \<union> connected_component_set (- S) a) g \<and>

What’s unfortunate is that the “negated exists” quantifier is available both 
for input and output in Isabelle, just not as a TeX macro.

I’ve pushed a fix. However, ideally this macro should be defined somehow and my 
change reverted.

isabelle-dev mailing list

Reply via email to