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 installation. Makarius