[isabelle-dev] \nexists

Tobias Nipkow nipkow at in.tum.de
Fri Jul 15 12:15:52 CEST 2016

LaTeX build problems are not infrequent and could be avoided easily if "build" 
produced the document by default.


On 14/07/2016 17:50, Lawrence Paulson wrote:
> 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
> This body part will be downloaded on demand.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160715/1f9acb95/attachment.bin>

More information about the isabelle-dev mailing list