[isabelle-dev] \nexists

[Lawrence Paulson]

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.

Larry
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160714/84ae2b56/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2016-07-14 at 16.44.00.png
Type: image/png
Size: 25059 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160714/84ae2b56/attachment-0001.png>