hoelzl at in.tum.de
Fri Jul 15 13:53:41 CEST 2016
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.
> 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
More information about the isabelle-dev