[isabelle-dev] \nexists

[Johannes Hölzl]

Am Freitag, den 15.07.2016, 12:15 +0200 schrieb Tobias Nipkow:
> LaTeX build problems are not infrequent and could be avoided easily
> if "build" 
> produced the document by default.
> 
> Tobias

+1

 - Johannes

> 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.
> > 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev