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