[isabelle-dev] \nexists

Makarius makarius at sketis.net
Sat Jul 16 16:24:40 CEST 2016

On 16/07/16 14:26, Tobias Nipkow wrote:
> But it turns out you are
> right: combining -a and -o document=pdf is not a good idea, it breaks
> Logics_ZF.

In which way does it fail?

I am running "isabelle build -a -o document=pdf" frequently. It should
definitely work.

It might be just an example of latex failure due to some odd latex


More information about the isabelle-dev mailing list