Tobias
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.
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
