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