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.


This body part will be downloaded on demand.

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to